equal
deleted
inserted
replaced
83 |
83 |
84 (*** Definitions used in the following rules ***) |
84 (*** Definitions used in the following rules ***) |
85 |
85 |
86 apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))" |
86 apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))" |
87 bot_def: "bot == (lam x. x`x)`(lam x. x`x)" |
87 bot_def: "bot == (lam x. x`x)`(lam x. x`x)" |
|
88 |
|
89 defs |
88 fix_def: "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" |
90 fix_def: "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" |
89 |
91 |
90 (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) |
92 (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) |
91 (* as a bisimulation. They can both be expressed as (bi)simulations up to *) |
93 (* as a bisimulation. They can both be expressed as (bi)simulations up to *) |
92 (* behavioural equivalence (ie the relations PO and EQ defined below). *) |
94 (* behavioural equivalence (ie the relations PO and EQ defined below). *) |
104 |
106 |
105 (*** Rules ***) |
107 (*** Rules ***) |
106 |
108 |
107 (** Partial Order **) |
109 (** Partial Order **) |
108 |
110 |
|
111 axioms |
109 po_refl: "a [= a" |
112 po_refl: "a [= a" |
110 po_trans: "[| a [= b; b [= c |] ==> a [= c" |
113 po_trans: "[| a [= b; b [= c |] ==> a [= c" |
111 po_cong: "a [= b ==> f(a) [= f(b)" |
114 po_cong: "a [= b ==> f(a) [= f(b)" |
112 |
115 |
113 (* Extend definition of [= to program fragments of higher type *) |
116 (* Extend definition of [= to program fragments of higher type *) |
134 (** The theory is non-trivial **) |
137 (** The theory is non-trivial **) |
135 distinctness: "~ lam x. b(x) = bot" |
138 distinctness: "~ lam x. b(x) = bot" |
136 |
139 |
137 (*** Definitions of Termination and Divergence ***) |
140 (*** Definitions of Termination and Divergence ***) |
138 |
141 |
|
142 defs |
139 Dvg_def: "Dvg(t) == t = bot" |
143 Dvg_def: "Dvg(t) == t = bot" |
140 Trm_def: "Trm(t) == ~ Dvg(t)" |
144 Trm_def: "Trm(t) == ~ Dvg(t)" |
141 |
145 |
142 text {* |
146 text {* |
143 Would be interesting to build a similar theory for a typed programming language: |
147 Would be interesting to build a similar theory for a typed programming language: |