equal
deleted
inserted
replaced
4 begin |
4 begin |
5 |
5 |
6 section {* The CBV Reduction Relation (Small-Step Semantics) *} |
6 section {* The CBV Reduction Relation (Small-Step Semantics) *} |
7 |
7 |
8 text {* |
8 text {* |
9 In order to help establishing the property that the CK Machine |
9 In order to help establishing the property that the Machine |
10 calculates a nomrmalform that corresponds to the evaluation |
10 calculates a normal form that corresponds to the evaluation |
11 relation, we introduce the call-by-value small-step semantics. |
11 relation, we introduce the call-by-value small-step semantics. |
12 *} |
12 *} |
13 |
13 |
14 inductive |
14 inductive |
15 cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) |
15 cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) |
104 |
104 |
105 section {* EXERCISE 9 *} |
105 section {* EXERCISE 9 *} |
106 |
106 |
107 text {* |
107 text {* |
108 The point of the cbv-reduction was that we can easily relatively |
108 The point of the cbv-reduction was that we can easily relatively |
109 establish the follwoing property: |
109 establish the following property: |
110 *} |
110 *} |
111 |
111 |
112 lemma machine_implies_cbvs_ctx: |
112 lemma machine_implies_cbvs_ctx: |
113 assumes a: "<e, Es> \<mapsto> <e', Es'>" |
113 assumes a: "<e, Es> \<mapsto> <e', Es'>" |
114 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |
114 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |