(* August 14, 1997 *)

(* script to be run when omnibus has been run *)

(* this file begins to implement a theory of programming *)

(* this should be considerably improved; it has a type of expressions
with the correct relationship to assignment (the original version of
assignment only allowed assignments of data constants to variables). *)

(* an important point is that function application in the Mark2 logic
is not extensional; forall@[(?f@?1)=?g@?1] does not necessarily imply
?f = ?g.  This means that the representation of programs and
expressions as "functions" does not wipe out structural information
about programs and expressions if it is done right.  Extensionality
does hold for functions built with brackets ([?P@?1]), so if we want
functions to be nonextensional, we do not define them using bracket
abstraction *)

(* this file begins to implement a theory of programming *)

declareconstant "data";  (* the type of storable data *)

axiom "NATDATA" "Nat:?x" "data:Nat:?x";  (* natural numbers can be data *)

axiom "BOOLDATA" "bool:?x" "data:bool:?x";  (* truth values can be data *)

declareconstant "error";  (* a data value signalling error *)

axiom "ERRORDATA" "error" "data:error";

axiom "ERRORNOTNAT" "error=Nat:error" "false";

axiom "ERRORNOTBOOL"  "error=bool:error" "false";

declareconstant "address";  (* the type of addresses *)

declareinfix "++";  (* the operation of shifting addresses up *)

(* this will be used in defining arrays *)

axiom "SHIFTUPTYPE" "?address ++ ?nat" "address:(address:?address)++(Nat:?nat)";

axiom "SHIFTUPASSOC" "(?address ++ ?nat1) ++ ?nat2" "?address ++ ?nat1 + ?nat2";

axiom "SHIFTSHIFTS" "(address:?a) = ?a++?n" "?n=0";

(* it may also be advisable to have "shift down"; more axioms may be needed *)

declareconstant "state";  (* states are functions from addresses to data *)

axiom "STATETYPE" "state:?s" "[data:?s@address:?1]";

(* note that equality between states is extensional *)

declareconstant "command"; (* commands are functions from states to states *)

(* but equality between commands is not necessarily extensional,
which allows commands to be treated as "text" objects where appropriate
(as in the definition of "allguards" below *)

axiom "COMMANDTYPE" "(command:?c)@?s" "state:?c@state:?s";

(* we introduce basic commands *)

(* the "skip" command does nothing *)

declareconstant "skip";

axiom "SKIPTYPE" "skip" "command:skip";

axiom "SKIP" "skip@?s" "state:?s";

(* the "abort" command throws us into total error *)

declareconstant "abort";

axiom "ABORTTYPE" "abort" "command:abort";

axiom "ABORT" "abort@?s" "[error]";  (* [error] is a completely useless state *)


axiom "ERRORINVARIANCE" "(command:?c)@[error]" "[error]";

(* this axiom expresses the uselessness of the state [error] *)

(* composition of programs *)

declareinfix ";";

axiom "PCOMPTYPE" "?c1;?c2" "command:(command:?c1);(command:?c2)";

axiom "PCOMP" "(?c1;?c2)@?s" "(command:?c2)@(command:?c1)@?s";

(* multiple assignment *)

(* implemented very abstractly; values at addresses satisfying a predicate
are copied from a given state; the state [error] cannot be modified *)

(* we develop a "left expression" type of predicates which can be
domains of multiple assignments *)

declareconstant "lexp";

defineinfix "DISJ_SUM" "?R,,?S" "[(~forsome@[bool:(?R@?2)&(?S@?2)])&(?R@?1)|?S@?1]";

(*

DISJ_SUM_1:

?R ,, [?1 = ?u] = 

[( ~?R @ ?u) & (?R @ ?1) | ?1 = ?u]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","DISJ_SUM0","EQBOOL","EQUATION","FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR","forall","forsome"]

*)

s "?R,,[?1=?u]";
ri "DISJ_SUM"; ex();
left();left();
dlls "CSYM";
ri "CSYM"; ex();
ri "LZ"; ex();
up();
rri "ANDBOOL"; ex();
up();up();
ri "FORSOMEDIST2"; ex();
left();
ri "DINSTANTIATEF1@?u"; ex();
ri "LEFT@EVAL**REFLEX"; ex();
ri "DSYM**DZER"; ex();
up();
ri "CSYM**CID"; ex();
up();
ri "NRULE2"; ex();
p "DISJ_SUM_1";

axiom "LEXP1" "[?1=address:?u]" "lexp:[?1=address:?u]";

axiom "LEXP2" "(lexp:?R),,(lexp:?S)" "lexp:(lexp:?R),,(lexp:?S)";

(* develop types "rexp" (right expression) and "rexp_state"
for assignment *)

declareconstant "rexp";  (* right expression:  selected functions
	from states to data:  nonextensional *)

declareconstant "rexp_state";  (* function from addresses to rexps *)

axiom "REXP_STATETYPE" "rexp_state:?x" "[rexp:?x@address:?1]";

(* develop some "right expressions" *)

axiom "REXP0" "(rexp:?x)@?s" "data:?x@state:?s";

defineconstant "con@?x" "[data:?x]";

axiom "REXP1" "con@?x" "rexp:con@?x";  (* data constants *)

defineconstant "var@?u" "[(state:?1)@(address:?u)]";

axiom "REXP2" "var@?u" "rexp:var@?u";

	(* contents of variables *)

defineinfix "EXPPLUS" "(?x!+!?y)@?s" "(Nat:(rexp:?x)@?s)+(Nat:(rexp:?y)@?s)";

	(* this is developed using definition facility rather than
	bracket abstraction to preserve the possibility of
	nonextensional operations like text substitution *)

axiom "REXP3" "?x!+!?y" "rexp:(rexp:?x)!+!rexp:?y";

	(* sums of expressions *)

defineinfix "ARRAYSUB" "(?v..?i)@?s" "(state:?s)@(address:?v)++(rexp:?i)@(state:?s)";

	(* array subscripting -- C style *)

(* this axiom expresses the idea that rexp_states are functions from
addresses to "rexps"; these in turn are functions from states to data *)

declareinfix "=::";  (* := cannot be used because initial colon is meaningful
			to Mark2 *)

axiom "MASSIGNTYPE" "?a =:: ?s" "command:(lexp:?a)=::rexp_state:?s"; 

axiom "MASSIGN" "(?a=::?s)@?t" 
"[((~(state:?t)=[error])&(lexp:?a)@address:?1)||(((rexp_state:?s)@(address:?1))@?t),(state:?t)@?1]";

(* single assignment *)

defineinfix "ONE_ASSIGN" "?v =: ?x" "[?1=address:?v]=::[rexp:?x]";

(*

ONE_ASSIGN_1:

((?v =: ?x) @ ?s) @ ?u = 

(( ~(state : ?s) = [error]) & (address : ?u) 
   = address : ?v) 
|| ((rexp : ?x) @ ?s) , (state : ?s) @ ?u

["AND","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","LEXP1","MASSIGN","NONTRIV","NOT","ONE_ASSIGN","REFLEX","REXP_STATETYPE","TYPES"]

*)



s "(?v=:?x)@?s";
ri "(LEFT@ONE_ASSIGN)**MASSIGN"; ex();
dlrs "LEXP1";
rri "LEXP1"; ex();
up();
ri "EVAL"; ex();
top();
right();right();left();left();left();
ri "REXP_STATETYPE"; ex();
right();
right();
ri "EVAL"; ex();
up();
ri "TYPES"; ex();
up();up();
ri "EVAL"; ex();
assigninto "?U" "?U@?u"; (* apply both sides of equation to ?u *)
ri "EVAL"; ex();
p "ONE_ASSIGN_1";

(* pair assignment *)

defineinfix "PAIR_ASSIGN" "(?u,?v) =,: ?x,?y" "([?1=address:?u]),,([?1=address:?v])=::[(?1=address:?u)||(data:?x),data:?y]";

(* this is much prettier than the previous version of pair assignment *)

(* the definition of ,, ensures that pair assignment will only have an effect
if the two addresses are distinct *)

(* real list assignment requires development *)

(* the next refinement needed here is the development of an expression type
to serve as the right side type of assignment statements instead of "state" *)

(* alternation *)

declareinfix "|:|";  (* links a guarded subcommand to a command *)

(* alternative commands will have a final "otherwise" clause *)

axiom "IFFITYPE" "(?b,?c)|:|?x" 
"command:([bool:?b@state:?1],command:?c)|:|command:?x";

(* the "execution behaviour" axiom given here is deterministic;
a nondeterministic axiom is harder to write, but certainly desirable *)

axiom "IFFI" "((?b,?c)|:|?x)@?s" "(?b@state:?s)||((command:?c)@?s),((command:?x)@?s)";

(* axioms for a function which extracts the "disjunction of the guards"
from a complex alternative statement.  Notice that the fact that commands
are _not_ treated as extensional functions from states to states means that we
can allow the extraction of structural information from commands = programs *)

declareconstant "allguards";

axiom "ALLGUARDS0" "allguards@abort" "[false]";

axiom "ALLGUARDS" "allguards@(?b,?c)|:|?x" "[(?b@state:?1)|((allguards@?x)@state:?1)]";

(* the use of allguards allows the definition of a guarded do loop
as an operation on the alternative statement expressing one step *)

declareconstant "loop";  (* transforms alternative statement into loop
statement *)

axiom "LOOPTYPE" "loop@?x" "command:loop@command:?x";

axiom "LOOP" "(loop@?c)@?s" "((allguards@?c)@state:?s)||((loop@?c)@(command:?c)@state:?s),state:?s";

axiom "TERMINATOR" "((allguards@?c)@(loop@?c)@?s)->[error]=(loop@?c)@?s" "true";

(* the axiom TERMINATOR guarantees that a loop either satisfies the
expected exit condition or aborts *)

axiom "INVARIANCE" "((?P @ state : ?s) & forall @ [(?P @ state : ?1) -> ?P @ (command : ?c) @ state : ?1]) -> (?P @ (loop @ ?c) @ ?s) | [error] = (loop @ ?c) @ ?s" "true";

(* the axiom INVARIANCE ensures that loop invariants hold when the
loop stops, unless it aborts *)

(*

ABORTCOMP1:

(?c ; abort) @ ?s = 

abort @ ?s

["ABORT","ABORTTYPE","PCOMP"]

*)

s "(?c;abort)@?s";
ri "PCOMP"; ex();
ri "LEFT@ $ABORTTYPE"; ex();
ri "ABORT"; ex();
initializecounter();
rri "ABORT"; ex();
assign "?s_1" "?s";
p "ABORTCOMP1";

(*

(abort ; ?c) @ ?s = 

abort @ ?s

["ABORT","ABORTTYPE","ERRORINVARIANCE","PCOMP"]

*)

s "(abort;?c)@?s";
ri "PCOMP"; ex();
ri "RIGHT@LEFT@ $ABORTTYPE"; ex();
ri "RIGHT@ABORT"; ex();
ri "ERRORINVARIANCE"; ex();
initializecounter();
rri "ABORT"; ex();
assign "?s_1" "?s";
p "ABORTCOMP2";

(*

SKIPCOMP1:

(skip ; ?c) @ ?s = 

(command : ?c) @ ?s

["COMMANDTYPE","PCOMP","SKIP","SKIPTYPE","TYPES"]

*)

s "(skip;?c)@?s";
ri "PCOMP"; ex();
ri "(RIGHT@LEFT@ $SKIPTYPE)**RIGHT@SKIP"; ex();
ri "COMMANDTYPE"; ex();
ri "RIGHT@RIGHT@ TYPES"; ex();
rri "COMMANDTYPE"; ex();
p "SKIPCOMP1";

(*

SKIPCOMP2:

(?c ; skip) @ ?s = 

(command : ?c) @ ?s

["COMMANDTYPE","PCOMP","SKIP","SKIPTYPE","TYPES"]

*)

 
s "(?c;skip)@?s";
ri "PCOMP"; ex();
ri "(LEFT@ $SKIPTYPE)**SKIP"; ex();
ri "(RIGHT@COMMANDTYPE) ** (EVERYWHERE@TYPES) ** $COMMANDTYPE"; ex();
p "SKIPCOMP2";

(* the preceding theorems are not strict equalities between programs because
programs are not extensional functions *)

(* we give a sample of a different kind of theorem *)

defineconstant "behaviour@?P" "[(command:?P)@?1]";

(* the behaviour operator gives the canonical function corresponding to
a program *)

(*

SKIPCOMP1a:

behaviour @ skip ; ?c = 

behaviour @ ?c

["COMMANDTYPE","PCOMP","PCOMPTYPE","SKIP","SKIPTYPE","TYPES","behaviour"]

*)

s "behaviour@skip;?c";
ri "behaviour"; ex();
ri "VALUE@[(EVERYWHERE@PCOMPTYPE) ** (EVERYWHERE@TYPES) ** (EVERYWHERE@ $PCOMPTYPE)]"; ex();
ri "VALUE@[SKIPCOMP1]"; ex();
rri "behaviour"; ex();
p "SKIPCOMP1a";

(*

PCOMPASSOC:

behaviour @ (?P ; ?Q) ; ?R = 

behaviour @ ?P ; ?Q ; ?R

["PCOMP","PCOMPTYPE","TYPES","behaviour"]

*)

s "behaviour@(?P;?Q);?R";
ri "behaviour"; ex();
right();left();
ri "(RIGHT@PCOMPTYPE)**TYPES** $PCOMPTYPE"; ex();
up();
ri "PCOMP"; ex();
right();left();
ri "(RIGHT@PCOMPTYPE)**TYPES** $PCOMPTYPE"; ex();
up();
ri "PCOMP"; ex();
top();right();
rri "PCOMP"; ex();
ri "(LEFT@TADDTOP@PCOMPTYPE)** $PCOMP"; ex();
up();
ri "VALUE@[LEFT@TADDTOP@PCOMPTYPE]"; ex();
rri "behaviour"; ex();
p "PCOMPASSOC";