0

1 
(* Title: CCL/ccl.thy


2 
ID: $Id$


3 
Author: Martin Coen


4 
Copyright 1993 University of Cambridge


5 


6 
Classical Computational Logic for Untyped Lambda Calculus with reduction to


7 
weak headnormal form.


8 


9 
Based on FOL extended with set collection, a primitive higherorder logic.


10 
HOL is too strong  descriptions prevent a type of programs being defined


11 
which contains only executable terms.


12 
*)


13 


14 
CCL = Gfp +


15 


16 
classes prog < term


17 


18 
default prog


19 


20 
types i 0


21 


22 
arities


23 
i :: prog


24 
fun :: (prog,prog)prog


25 


26 
consts


27 
(*** Evaluation Judgement ***)


28 
">" :: "[i,i]=>prop" (infixl 20)


29 


30 
(*** Bisimulations for preorder and equality ***)


31 
"[=" :: "['a,'a]=>o" (infixl 50)


32 
SIM :: "[i,i,i set]=>o"


33 
POgen,EQgen :: "i set => i set"


34 
PO,EQ :: "i set"


35 


36 
(*** Term Formers ***)


37 
true,false :: "i"


38 
pair :: "[i,i]=>i" ("(1<_,/_>)")


39 
lambda :: "(i=>i)=>i" (binder "lam " 55)


40 
case :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"


41 
"`" :: "[i,i]=>i" (infixl 56)


42 
bot :: "i"


43 
fix :: "(i=>i)=>i"


44 


45 
(*** Defined Predicates ***)


46 
Trm,Dvg :: "i => o"


47 


48 
rules


49 


50 
(******* EVALUATION SEMANTICS *******)


51 


52 
(** This is the evaluation semantics from which the axioms below were derived. **)


53 
(** It is included here just as an evaluator for FUN and has no influence on **)


54 
(** inference in the theory CCL. **)


55 


56 
trueV "true > true"


57 
falseV "false > false"


58 
pairV "<a,b> > <a,b>"


59 
lamV "lam x.b(x) > lam x.b(x)"


60 
caseVtrue "[ t > true; d > c ] ==> case(t,d,e,f,g) > c"


61 
caseVfalse "[ t > false; e > c ] ==> case(t,d,e,f,g) > c"


62 
caseVpair "[ t > <a,b>; f(a,b) > c ] ==> case(t,d,e,f,g) > c"


63 
caseVlam "[ t > lam x.b(x); g(b) > c ] ==> case(t,d,e,f,g) > c"


64 


65 
(*** Properties of evaluation: note that "t > c" impies that c is canonical ***)


66 


67 
canonical "[ t > c; c==true ==> u>v; \


68 
\ c==false ==> u>v; \


69 
\ !!a b.c==<a,b> ==> u>v; \


70 
\ !!f.c==lam x.f(x) ==> u>v ] ==> \


71 
\ u>v"


72 


73 
(* Should be derivable  but probably a bitch! *)


74 
substitute "[ a==a'; t(a)>c(a) ] ==> t(a')>c(a')"


75 


76 
(************** LOGIC ***************)


77 


78 
(*** Definitions used in the following rules ***)


79 


80 
apply_def "f ` t == case(f,bot,bot,%x y.bot,%u.u(t))"


81 
bot_def "bot == (lam x.x`x)`(lam x.x`x)"


82 
fix_def "fix(f) == (lam x.f(x`x))`(lam x.f(x`x))"


83 


84 
(* The preorder ([=) is defined as a simulation, and behavioural equivalence (=) *)


85 
(* as a bisimulation. They can both be expressed as (bi)simulations up to *)


86 
(* behavioural equivalence (ie the relations PO and EQ defined below). *)


87 


88 
SIM_def


89 
"SIM(t,t',R) == (t=true & t'=true)  (t=false & t'=false)  \


90 
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R)  \


91 
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"


92 


93 
POgen_def "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot  SIM(t,t',R))}"


94 
EQgen_def "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot  SIM(t,t',R))}"


95 


96 
PO_def "PO == gfp(POgen)"


97 
EQ_def "EQ == gfp(EQgen)"


98 


99 
(*** Rules ***)


100 


101 
(** Partial Order **)


102 


103 
po_refl "a [= a"


104 
po_trans "[ a [= b; b [= c ] ==> a [= c"


105 
po_cong "a [= b ==> f(a) [= f(b)"


106 


107 
(* Extend definition of [= to program fragments of higher type *)


108 
po_abstractn "(!!x. f(x) [= g(x)) ==> (%x.f(x)) [= (%x.g(x))"


109 


110 
(** Equality  equivalence axioms inherited from FOL.thy **)


111 
(**  congruence of "=" is axiomatised implicitly **)


112 


113 
eq_iff "t = t' <> t [= t' & t' [= t"


114 


115 
(** Properties of canonical values given by greatest fixed point definitions **)


116 


117 
PO_iff "t [= t' <> <t,t'> : PO"


118 
EQ_iff "t = t' <> <t,t'> : EQ"


119 


120 
(** Behaviour of noncanonical terms (ie case) given by the following betarules **)


121 


122 
caseBtrue "case(true,d,e,f,g) = d"


123 
caseBfalse "case(false,d,e,f,g) = e"


124 
caseBpair "case(<a,b>,d,e,f,g) = f(a,b)"


125 
caseBlam "case(lam x.b(x),d,e,f,g) = g(b)"


126 
caseBbot "case(bot,d,e,f,g) = bot" (* strictness *)


127 


128 
(** The theory is nontrivial **)


129 
distinctness "~ lam x.b(x) = bot"


130 


131 
(*** Definitions of Termination and Divergence ***)


132 


133 
Dvg_def "Dvg(t) == t = bot"


134 
Trm_def "Trm(t) == ~ Dvg(t)"


135 


136 
end


137 


138 


139 
(*


140 
Would be interesting to build a similar theory for a typed programming language:


141 
ie. true :: bool, fix :: ('a=>'a)=>'a etc......


142 


143 
This is starting to look like LCF.


144 
What are the advantages of this approach?


145 
 less axiomatic


146 
 wfd induction / coinduction and fixed point induction available


147 


148 
*)
