--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "hap_reduction.ma".
+
+(* KASHIMA'S "HAP" COMPUTATION **********************************************)
+
+(* Note: this is the "head in application" computation of:
+ R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
+*)
+definition hap: relation term ≝ star … hap1.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "labelled_sequential_reduction.ma".
+
+(* KASHIMA'S "HAP" COMPUTATION (SINGLE STEP) ********************************)
+
+(* Note: this is one step of the "head in application" computation of:
+ R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
+*)
+inductive hap1: relation term ≝
+| hap1_beta: ∀B,A. hap1 (@B.𝛌.A) ([⬐B]A)
+| hap1_appl: ∀B,A1,A2. hap1 A1 A2 → hap1 (@B.A1) (@B.A2)
+.
+
+lemma hap1_lift: liftable hap1.
+#h #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
+#B #A #d <dsubst_lift_le //
+qed.
+
+lemma hap1_inv_lift: deliftable hap1.
+#h #N1 #N2 #H elim H -N1 -N2
+[ #D #C #d #M1 #H
+ elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
+ elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
+| #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B #A1 #H1 #H2 #H destruct
+ elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #H destruct (**) (* simplify line *)
+ @(ex2_1_intro … (@B.A2)) // /2 width=1/
+]
+qed-.
+
+lemma hap1_dsubstable: dsubstable_dx hap1.
+#D1 #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
+#D2 #A #d >dsubst_dsubst_ge //
+qed.
+
+lemma hap1_lsred: ∀M,N. hap1 M N →
+ ∃∃p. in_spine p & M ⇀[p] N.
+#M #N #H elim H -M -N /2 width=3/
+#B #A1 #A2 #_ * /3 width=3/
+qed-.
F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
*)
-inductive lsred: rpointer → relation term ≝
-| lsred_beta : ∀A,D. lsred (◊) (@D.𝛌.A) ([⬐D]A)
+inductive lsred: rptr → relation term ≝
+| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A)
| lsred_abst : ∀p,A,C. lsred p A C → lsred p (𝛌.A) (𝛌.C)
| lsred_appl_sn: ∀p,B,D,A. lsred p B D → lsred (true::p) (@B.A) (@D.A)
| lsred_appl_dx: ∀p,B,A,C. lsred p A C → lsred (false::p) (@B.A) (@B.C)
lemma lsred_inv_vref: ∀p,M,N. M ⇀[p] N → ∀i. #i = M → ⊥.
#p #M #N * -p -M -N
-[ #A #D #i #H destruct
+[ #B #A #i #H destruct
| #p #A #C #_ #i #H destruct
| #p #B #D #A #_ #i #H destruct
| #p #B #A #C #_ #i #H destruct
lemma lsred_inv_beta: ∀p,M,N. M ⇀[p] N → ∀D,C. @D.C = M → ◊ = p →
∃∃A. 𝛌.A = C & [⬐D] A = N.
#p #M #N * -p -M -N
-[ #A #D #D0 #C0 #H #_ destruct /2 width=3/
+[ #B #A #D0 #C0 #H #_ destruct /2 width=3/
| #p #A #C #_ #D0 #C0 #H destruct
| #p #B #D #A #_ #D0 #C0 #_ #H destruct
| #p #B #A #C #_ #D0 #C0 #_ #H destruct
lemma lsred_inv_abst: ∀p,M,N. M ⇀[p] N → ∀A. 𝛌.A = M →
∃∃C. A ⇀[p] C & 𝛌.C = N.
#p #M #N * -p -M -N
-[ #A #D #A0 #H destruct
+[ #B #A #A0 #H destruct
| #p #A #C #HAC #A0 #H destruct /2 width=3/
| #p #B #D #A #_ #A0 #H destruct
| #p #B #A #C #_ #A0 #H destruct
lemma lsred_inv_appl_sn: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → true::q = p →
∃∃D. B ⇀[q] D & @D.A = N.
#p #M #N * -p -M -N
-[ #A #D #B0 #A0 #p0 #_ #H destruct
+[ #B #A #B0 #A0 #p0 #_ #H destruct
| #p #A #C #_ #B0 #D0 #p0 #H destruct
| #p #B #D #A #HBD #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/
| #p #B #A #C #_ #B0 #A0 #p0 #_ #H destruct
lemma lsred_inv_appl_dx: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → false::q = p →
∃∃C. A ⇀[q] C & @B.C = N.
#p #M #N * -p -M -N
-[ #A #D #B0 #A0 #p0 #_ #H destruct
+[ #B #A #B0 #A0 #p0 #_ #H destruct
| #p #A #C #_ #B0 #D0 #p0 #H destruct
| #p #B #D #A #_ #B0 #A0 #p0 #_ #H destruct
| #p #B #A #C #HAC #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/
lemma lsred_fwd_mult: ∀p,M,N. M ⇀[p] N → #{N} < #{M} * #{M}.
#p #M #N #H elim H -p -M -N
-[ #A #D @(le_to_lt_to_lt … (#{A}*#{D})) //
+[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) //
normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *)
| //
| #p #B #D #A #_ #IHBD
lemma lsred_lift: ∀p. liftable (lsred p).
#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#A #D #d <dsubst_lift_le //
+#B #A #d <dsubst_lift_le //
qed.
lemma lsred_inv_lift: ∀p. deliftable (lsred p).
#p #h #N1 #N2 #H elim H -p -N1 -N2
-[ #C #D #d #M1 #H
+[ #D #C #d #M1 #H
elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
| #p #C1 #C2 #_ #IHC12 #d #M1 #H
lemma lsred_dsubst: ∀p. dsubstable_dx (lsred p).
#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#A #D2 #d >dsubst_dsubst_ge //
+#D2 #A #d >dsubst_dsubst_ge //
qed.
theorem lsred_mono: ∀p. singlevalued … (lsred p).
#p #M #N1 #H elim H -p -M -N1
-[ #A #D #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *)
+[ #B #A #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *)
| #p #A #C #_ #IHAC #N2 #H elim (lsred_inv_abst … H ??) -H [3: // |2: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *)
| #p #B #D #A #_ #IHBD #N2 #H elim (lsred_inv_appl_sn … H ?????) -H [5,6: // |2,3,4: skip ] #D0 #HBD #H destruct /3 width=1/ (**) (* simplify line *)
| #p #B #A #C #_ #IHAC #N2 #H elim (lsred_inv_appl_dx … H ?????) -H [5,6: // |2,3,4: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *)
h : relocation height
i, j : de Bruijn index
k : relocation height
+m, n : measures on terms
p, q : redex pointer
r, s : redex pointer sequence
definition confluent: ∀A. predicate (relation A) ≝ λA,R.
∀a0. confluent1 … R a0.
+(* booleans *)
+
+definition is_false: predicate bool ≝ λb.
+ false = b.
+
(* arithmetics *)
lemma lt_refl_false: ∀n. n < n → ⊥.
notation > "◊"
non associative with precedence 90
for @{'nil}.
+
+let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
+].
on application nodes, "false" means "proceed right"
and "true" means "proceed left"
*)
-definition rpointer: Type[0] ≝ list bool.
+definition rptr: Type[0] ≝ list bool.
+
+(* Note: a redex is "in the spine" when is not in the argument of an application *)
+definition in_spine: predicate rptr ≝ λp.
+ All … is_false p.
(* Note: precedence relation on redex pointers: p ≺ q
to serve as base for the order relations: p < q and p ≤ q *)
-inductive rpprec: relation rpointer ≝
+inductive rpprec: relation rptr ≝
| rpprec_nil : ∀b,q. rpprec (◊) (b::q)
| rppprc_cons: ∀p,q. rpprec (false::p) (true::q)
| rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q)
for @{ 'prec $a $b }.
(* Note: this is p < q *)
+definition rplt: relation rptr ≝ TC … rpprec.
+
interpretation "'less than' on redex pointers"
- 'lt p q = (TC rpointer rpprec p q).
+ 'lt p q = (rplt p q).
(* Note: this is p ≤ q *)
+definition rple: relation rptr ≝ star … rpprec.
+
interpretation "'less or equal to' on redex pointers"
- 'leq x y = (star rpointer x y).
+ 'leq p q = (rple p q).
(* Policy: pointer sequence metavariables: r, s *)
-definition rpseq: Type[0] \def list rpointer.
+definition rpseq: Type[0] \def list rptr.
+
+(* Note: a "spine" computation contracts just redexes in the spine *)
+definition is_spine: predicate rpseq ≝ λs.
+ All … in_spine s.
+
+(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
+definition is_le: predicate rpseq ≝ λs.
+ Allr … rple s.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "hap_computation.ma".
+
+(* KASHIMA'S "ST" COMPUTATION ***********************************************)
+
+(* Note: this is the "standard" computation of:
+ R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
+*)
+inductive st: relation term ≝
+| st_vref: ∀M,i. hap M (#i) → st M (#i)
+| st_abst: ∀M,A,C. hap M (𝛌.A) → st A C → st M (𝛌.C)
+| st_appl: ∀M,B,D,A,C. hap M (@B.A) → st B D → st A C → st M (@D.C)
+.
+
projects / helm.git / commitdiff