Transcript Imperative Program with Input

Imperative Program with Input
http://cis.k.hosei.ac.jp/~yukita/
Imperative Programs
Let  be an alphabet and consider functors from free monoid on
 to Sets.
Such a functor can be considered as a collection of functions
f a : X  X (a  ) for a fixed set X ( the state space) with
the property f ba  f b  f a for all pairs a, b  .
If | X | , we call such a functor
a deterministic finite automaton or deterministic finite machine.
2
Def. Finite State Recognizer
A finite state recognizer is a finite state automaton with
one specified start state J and a finite set K1 , K 2 , of
specified end states.
A recognizer defines a subset U of * as follows :
an an 1  a1  U
if
f an  f a2 f a1 ( J )  K i
for some end state K i .
3
Theorem.
The set U  * is recognized by a finite state recognizer
if and only if U is a regular language.
Proof. A recognizer is a special type of regular grammar. ...
Conversely , given a grammar X (without  ), we show how
to construct an automaton which recognizes the same language
as that generated by the grammar.
Take the states of the automaton to be 2obj X .
Put an arrow a : Y1  Y2
if Y2  { y2 | y1  Y1 ;  a : y1  y2 in the grammar}.
Take the start state to be {J }. Take the end states to be all
subsets containing at least one end object of the grammar.
4
Imperative Program with Input
Def. Given an aphabet , an imperative program with input from 
is a functor *  Sets, constructe d out of given functions using the
operations available in a distributi ve category.
Giving such a functor amounts to giving a set X (the state space)
and functions f a : X  X (a  ) constructe d from given functions
in the appropriat e way.
A behavior of an implerativ e program consists of the effect of a sequence
of inputs on an initial state.
a3
a2
a1

x2 
x1 
x0 
f
f
f
5
Ex. 37. Exponential
The state space is X    ( I  I ).
The input alphabet is   {clock }  . Notice |  | .
Let ( p, d , t ) be a typical element of X .
Rough idea :
clock
number
t  0 calculatio n takes place
ignore
t 1
ignore
number input
6
Ex. 37 continued
f clock :   ( I  I )    ( I  I )
2
2
( p  d , d  1,0)
( p , d ,0 )  
( p, d ,1)
if d  1
if d  1
( p, d ,1)  ( p, d ,1).
fn :   (I  I )    (I  I )
2
2
( p , d ,0 )  ( p , d ,0)
( p, d ,1)  (1, n,0).
7
Ex. 38. Product and Sum
We start with the following two programs.
f a : X  X with 1  {a}.
f b : X  X with  2  {b}.
  1   2
New program 1 :
g a  f a 1Y : X  Y  X  Y ,
g b  1X  f b : X  Y  X  Y .
New program 2 :
ha  f a  1Y : X  Y  X  Y ,
hb  1X  f b : X  Y  X  Y .
8
Ex. 38. continued
Program 1 allows the two users to work independen tly.
Program 2 put the two users in total conflict.
If the initial state belongs to the first component of X  Y
then every input from the first user has effect; no input of
the second user has effect.
If the initial state belongs to the second component then
the roles are reversed.
9
Basic Idea behind Functional
Languages
• The move towards programming by
specification of goals or functions,
• as distinct from imperative programming.
• In many cases, the specification actually
contains the means for computation.
10
Ex. 39 f(x)=2x
Graph Data has two objects I and N and two arrows
0 : I  N (zero) ,
s : N  N (successor ).
Graph Function　contains Data and one extra arrow
f : N  N.
The set of equations between paths Equation consists of
fs  ssf ,
f 0  0.
11
Def. Functional Specification
A functional specification consists of two graphs,
Data  Function,
and a set, Equation, of equations between paths in Function.
Data has three specified objects, I, J, K ; Function has a
specified arrow f : J  K .
A funtional specificat ion determines a relation
f : PathsData ( I , J )  PathsData ( I , K )
as follows : f ( path1)  path2 if f ( path1)  path2 is
deducible in Function from the equations in Equation.
12
Ex. 40. Calculation in Ex. 39
We let J  K  N .
f : Paths( I , N )  Paths( I , N )
s n 0  s m 0,
if fs n 0  s m 0 is deducible from fs  ssf and f 0  0.
It is clear that
f : s n 0  s 2n 0.
13
Note.
• A functional specification may give rise to
a partial function instead of a (full) function,
• or even a multi-valued function.
• Robbie Gates showed that the partial
functions specifiable from  to  are
precisely the partial recursive functions.
14
Ex. 41. Length of a list
Let Data has three objects I, L, and N and arrows
0 : I  N,
o : I  L,
s:N  N
a1 , a2 , a3 , : L  L.
Think of o as the empty list, and each letter a as appending
a letter to the list.
Function consists of Data together with one extra arrow
length : L  N .
Equation consists of two equations :
length  ai  s  length
(ai  ),
length  o  0.
15
Ex. 41. continued
length : Paths( I , L)  Paths( I , N ) gives the length of a list.
A typical calculatio n goes like this :
length  a1  a3  a3  a2  o  s  length  a3  a3  a2  o
 s  s  length  a3  a2  o
 s  s  s  length  a2  o
 s  s  s  s  length  o
 s  s  s  s  0  s 4 0.
16
Ex. 42. Sort
The alphabet  is ordered as a1  a2  a3  .
Data consists of two objects I and L and arrows
o : I  L, a1 , a2 , a3 , : L  L.
Function has two extra arrows :
transfer : L  L and sort : L  L.
Arrow transfer is intended to alter a list in the following
way : it takes the leftmost element of a list and moves it
to the left of the first element wh ich is larger or the same.
17
Ex. 42. continued
Equation consists of
sort  o  o,
sort  a  transfer  a  sort
transfer  o  o,
transfer  a  o  a  o,
transfer  ai  a j  ai  a j
transfer  ai  a j  a j  transfer  ai
(a  ),
(ai  a j ),
(ai  a j ).
sort : Paths( I , L)  Paths( I , L) sorts a list into
ascending order.
18
Ex. 42. A typical calculation
sort  a2  a1  a3  a1  o
 transfer  a2  sort  a1  a3  a1  o
 transfer  a2  transfer  a1  sort  a3  a1  o
 transfer  a2  transfer  a1  transfer  a3  sort  a1  o
 transfer  a2  transfer  a1  transfer  a3  transfer  a1  sort  o
 transfer  a2  transfer  a1  transfer  a3  transfer  a1  o
 transfer  a2  transfer  a1  transfer  a3  a1  o
 transfer  a2  transfer  a1  a1  transfer  a3  o
 transfer  a2  transfer  a1  a1  a3  o
 transfer  a2  a1  a1  a3  o
 a1  transfer  a2  a1  a3  o
 a1  a1  transfer  a2  a3  o
 a1  a1  a2  a3  o
19