Our definition of a language as a propositional function captures the intuition that to know a
language is to know the criteria for saying when a sentence is in it.
To say
is in the language is to know how to prove
. This
agrees with Hopcroft and Ullman; they are concerned with certain
special ways of knowing
.
One especially simple kind of representation of arises when the
proposition is decidable, that is when there is a function
:
list
such that
Such a language is called decidable or recursive.
Another way to represent a language with a function is to provide
an enumeration of
, that is a function
such that
The function can also be said to represent
.
Given the function an interesting procedure arises for
specifying a language, the procedure is called a (real) recognizer. To specify
, we write a function
Hopcroft and Ullman go on to show that given a real recognizer, we can
also define an enumerator. Basically we enumerate . We do this uniformly only if the type is non-empty.
Then given
, there is an operation
which produces a
function from
onto
. Since we are interested mainly in
automata and the Myhill-Nerode theorem of Chapter 3, we skip over
Chapter 2 on Grammars although it would not be difficult to formalize
all of the results there. (The only interesting result is Theorem 2.2-a context sensitive grammar is recursive.)