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 head-normal form.
|
|
8 |
|
|
9 |
Based on FOL extended with set collection, a primitive higher-order 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 |
|
283
|
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 pre-order 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 pre-order ([=) 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 non-canonical terms (ie case) given by the following beta-rules **)
|
|
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 non-trivial **)
|
|
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 |
*)
|