|
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 |
|
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 *) |