Notes on lecture 11, (Tuesday, February 25), specifying
automata by Westerly Weimer.

"What can you say in First-Order logic?" Almost anything can be specified
in this language. Turing machines, the Post correspondence problem,
and automata can all be described. First-order logic is so
expressive that its validity problem cannot be decided. 

Specifying An Automaton

Formally, a finite automaton is characterized by the 5-touple
	<S, Sigma, Delta, q0, F>
Where: 	S is the set of states
	Sigma is the set of input symbols
	Delta is the transition function, mapping SxSigma -> S (given
	a state and an input it yields a new state)
	q0 is an element of S and denotes the starting state
	F is a subset of S and denotes the set of final (accepting)
	states.

S and Sigma must be disjoint.

In general a finite automaton starts at state q0, receives an input i (an
element of Sigma), computes a new state based on the result of
Delta(current state, i), sets that new state to be the current state, and
looks for more input. When the input stream ends the automaton is said to
have "accepted" the input if it is currently in a state that is an element
of F.

We will not try to say what "finite" means in this lecture, and thus
we formalize a more general notion of automaton. But we can specify
specific finite automata as we show at the end.

It is often convenient to speak of automata accepting entire lists made up
of elements of sigma. Delta* is a function mapping S x Sigma* -> S
representing the final state of an automaton after receiving Sigma*, an
ordered list of elements from Sigma.

Using the standard formulations for equality and uniqueness, we can
formalize this notion of a list: (where Exy means x and y are equal)

	N(x)		"x is Nil (the special marker terminating a list)"
	L(x)		"x is a list"
	A(x)		"x is an atom (an element in a list)"
	Cons(x,y,z)	"z is the list that results from prepending x,
			 an atom, onto y, a list."

	(E!n) N(n)	"there exists a unique Nil element"
	(Ax) [ N(x) => L(x) ]	"the Nil element is a list"
	(Ah)(Al) [( A(h) & L(l) ) => ( (E!z) Cons(h,l,z) )]
			"for any atom and list there is a unique list
			formed by prepending the atom to the list"
	(Az) [ L(z) & ~N(z) ] => (E!h)(E!l) A(h)&L(l)&Cons(h,l,z)
			"any non-nil list was constructed from a unique
			atom and list (called the head and tail)"

	(Ax)(Ay) Exy & N(x) => N(y)		"substitution"
	(Ax)(Ay) Exy & L(x) => L(y)	 	...
	(Ax)(Ay) Exy & A(x) => A(y)
	(AX)(Ax)(Ay)(Az) ExX & Cons(x,y,z) => Cons(X,y,z)
	(Ax)(Ay)(AY)(Az) EyY & Cons(x,y,z) => Cons(x,Y,z)
	(Ax)(Ay)(Az)(AZ) EzZ & Cons(x,y,z) => Cons(x,y,Z)
	
Sigma* is then a list where all the atoms are elements of Sigma.

	State(x)	"x is a state (an element of S)"
	Symbol(x)	"x is a symbol (an element of Sigma)"
	Final(x)	"x is a final state (an element of F)"
	Q0(x)		"x is a start state"
	Delta(s,a,z)	"Delta(s,a) == z"
	DeltaStar(s,a,z)"DeltaStar(s,a) == z, where a is a list of symbols"

	(Ax)(AX) ExX & State(x) => State(X)
	(Ax)(AX) ExX & Symbol(x) => Symbol(X)
	(Ax)(AX) ExX & Final(x) => Final(X)
	(Ax)(AX) ExX & Q0(x) => Q0(X)

	(E!x) (State(x) & Q0(x)) "there is a unique start state"
	
	(As)(Aa) State(s) & Symbol(a) => (E!z)[State(z) & Delta(s,a,z)]	
			"Delta is a single valued total function"

	(As)(AS)(Aa)(Az) EsS & Delta(s,a,z) => Delta(S,a,z) 
	(As)(Aa)(AA)(Az) EaA & Delta(s,a,z) => Delta(s,A,z)
	(As)(Aa)(Az)(AZ) EzZ & Delta(s,a,z) => Delta(s,a,Z)

	(As)(An) Nil(n) & State(s) => DeltaStar(s,n,s)
		"DeltaStar(s,Nil) = s"

	(Ax)(Eh)(El)(Eq)(As')(As) List(x) & Cons(h,l,x) & State(q) &
		Delta(s,h,q) & DeltaStar(q,l,s') & Symbol(h) & List(l)
		=> DeltaStar(s,x,s')

		"DeltaStar(s, head.tail) = DeltaStar(Delta(s,head),tail)"

	(As)(AS)(Aa)(Az) EsS & DeltaStar(s,a,z) => DeltaStar(S,a,z) 
	(As)(Aa)(AA)(Az) EaA & DeltaStar(s,a,z) => DeltaStar(s,A,z)
	(As)(Aa)(Az)(AZ) EzZ & DeltaStar(s,a,z) => DeltaStar(s,a,Z)

	Accept(w)	"This automata accepts (finishes in a final state)
			on input w, a list of symbols."
			
	(Aw) [ List(w) & Accept(w) <=> (Aq)(Es) State(s) & Q0(q) &
					DeltaStar(q0,w,s) & Final(s) ]

	(Aw)(AW) EwW & Accept(w) => Accept(W)

	(Ax) State(x) => ~Symbol(x) "states and symbols are disjoint"
	

As a specific example, to specify the finite automaton that accepts the
regular expression "[b*]|[ab*a]"

	/   State ==> a ==> State  \ 
        |b  || 		    ||     | b
	\-> Q     <== a <== R    <-/

We assert:
	(Ea)(Eb)(Eq)(Ew)
		Symbol(a) & Symbol(b) & ~Eab
		State(q) & State(r) & ~Eqr
		Delta(q,a,r)
		Delta(q,b,b)
		Delta(r,a,q)
		Delta(r,b,r) 
		Start(q)
		Final(q)

We can then ask questions like:
	Is DeltaStar(q, 'ab', r) true?
And answer them by instantiating quantifiers to obtain specific values.
For example, we know:
		
	(Ax)(Eh)(El)(Eq)(As')(As) List(x) & Cons(h,l,x) & State(q) &
		Delta(s,h,q) & DeltaStar(q,l,s') & Symbol(h) & List(l)
		=> DeltaStar(s,x,s')

So if we additionally assert
	(El)(En) List(l) & Nil(n) & List(n) & Cons(a,n,l)
Then we already have
		State(q) & Delta(q,a,r) & Symbol(a)
And from 
	(As)(An) Nil(n) & State(s) => DeltaStar(s,n,s)
we can instantiate
		Nil(n) & State(r) => DeltaStar(r,n,r)
and apply modus ponens:
		DeltaStar(r,n,r)
and again to get:
		DeltaStar(q,l,r)
Which tells us (correctly) that DeltaStar(q, 'a') -> 'r'.

This procedure could be extended to show that 
	DeltaStar(q, 'ab', r)
is a logical consequence of the formulae representing the character of
finite automata in general and this example automaton in specific. Such a
formal specification makes it possible to prove statements about the
nature and behavior of automata, or any other formalized concept.