matita/matita/contribs/lambda/st_computation.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "labelled_hap_computation.ma".
  16
  17 (* KASHIMA'S "ST" COMPUTATION ***********************************************)
  18
  19 (* Note: this is the "standard" computation of:
  20          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
  21 *)
  22 inductive st: relation term ≝
  23 | st_vref: ∀s,M,i. M ⓗ⇀*[s] #i → st M (#i)
  24 | st_abst: ∀s,M,A1,A2. M ⓗ⇀*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
  25 | st_appl: ∀s,M,B1,B2,A1,A2. M ⓗ⇀*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
  26 .
  27
  28 interpretation "'st' computation"
  29     'Std M N = (st M N).
  30
  31 notation "hvbox( M ⓢ⥤* break term 46 N )"
  32    non associative with precedence 45
  33    for @{ 'Std $M $N }.
  34
  35 axiom st_refl: reflexive … st.
  36
  37 axiom st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ⥤* N2.
  38
  39 axiom st_lift: liftable st.
  40
  41 axiom st_inv_lift: deliftable_sn st.
  42
  43 axiom st_dsubst: dsubstable st.