54 (** inference in the theory CCL. **) |
54 (** inference in the theory CCL. **) |
55 |
55 |
56 trueV "true ---> true" |
56 trueV "true ---> true" |
57 falseV "false ---> false" |
57 falseV "false ---> false" |
58 pairV "<a,b> ---> <a,b>" |
58 pairV "<a,b> ---> <a,b>" |
59 lamV "lam x.b(x) ---> lam x.b(x)" |
59 lamV "lam x. b(x) ---> lam x. b(x)" |
60 caseVtrue "[| t ---> true; d ---> c |] ==> case(t,d,e,f,g) ---> c" |
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" |
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" |
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" |
63 caseVlam "[| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c" |
64 |
64 |
65 (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***) |
65 (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***) |
66 |
66 |
67 canonical "[| t ---> c; c==true ==> u--->v; |
67 canonical "[| t ---> c; c==true ==> u--->v; |
68 c==false ==> u--->v; |
68 c==false ==> u--->v; |
69 !!a b.c==<a,b> ==> u--->v; |
69 !!a b. c==<a,b> ==> u--->v; |
70 !!f.c==lam x.f(x) ==> u--->v |] ==> |
70 !!f. c==lam x. f(x) ==> u--->v |] ==> |
71 u--->v" |
71 u--->v" |
72 |
72 |
73 (* Should be derivable - but probably a bitch! *) |
73 (* Should be derivable - but probably a bitch! *) |
74 substitute "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')" |
74 substitute "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')" |
75 |
75 |
76 (************** LOGIC ***************) |
76 (************** LOGIC ***************) |
77 |
77 |
78 (*** Definitions used in the following rules ***) |
78 (*** Definitions used in the following rules ***) |
79 |
79 |
80 apply_def "f ` t == case(f,bot,bot,%x y.bot,%u.u(t))" |
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)" |
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))" |
82 fix_def "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" |
83 |
83 |
84 (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) |
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 *) |
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). *) |
86 (* behavioural equivalence (ie the relations PO and EQ defined below). *) |
87 |
87 |
88 SIM_def |
88 SIM_def |
89 "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) | |
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) | |
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))" |
91 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))" |
92 |
92 |
93 POgen_def "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}" |
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))}" |
94 EQgen_def "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}" |
95 |
95 |
96 PO_def "PO == gfp(POgen)" |
96 PO_def "PO == gfp(POgen)" |
120 (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **) |
120 (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **) |
121 |
121 |
122 caseBtrue "case(true,d,e,f,g) = d" |
122 caseBtrue "case(true,d,e,f,g) = d" |
123 caseBfalse "case(false,d,e,f,g) = e" |
123 caseBfalse "case(false,d,e,f,g) = e" |
124 caseBpair "case(<a,b>,d,e,f,g) = f(a,b)" |
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)" |
125 caseBlam "case(lam x. b(x),d,e,f,g) = g(b)" |
126 caseBbot "case(bot,d,e,f,g) = bot" (* strictness *) |
126 caseBbot "case(bot,d,e,f,g) = bot" (* strictness *) |
127 |
127 |
128 (** The theory is non-trivial **) |
128 (** The theory is non-trivial **) |
129 distinctness "~ lam x.b(x) = bot" |
129 distinctness "~ lam x. b(x) = bot" |
130 |
130 |
131 (*** Definitions of Termination and Divergence ***) |
131 (*** Definitions of Termination and Divergence ***) |
132 |
132 |
133 Dvg_def "Dvg(t) == t = bot" |
133 Dvg_def "Dvg(t) == t = bot" |
134 Trm_def "Trm(t) == ~ Dvg(t)" |
134 Trm_def "Trm(t) == ~ Dvg(t)" |