Documentation

Cslib.Languages.CombinatoryLogic.Evaluation

Evaluation results #

This file formalises evaluation and normal forms of SKI terms.

Main definitions #

Main results #

References #

This file draws heavily from https://gist.github.com/b-mehta/e412c837818223b8f16ca0b4aa19b166.

source
def Cslib.SKI.RedexFree :
SKI → Prop

The predicate that a term has no reducible sub-terms.

Equations
Instances For
    source
    def Cslib.SKI.evalStep (x : SKI) :
    PLift x.RedexFree ⊕ SKI

    One-step evaluation as a function: either it returns a term that has been reduced by one step, or a proof that the term is redex free. Uses normal-order reduction.

    Equations
    Instances For
      source
      theorem Cslib.SKI.evalStep_right_correct (x y : SKI) :
      x.evalStep = Sum.inr y → RedSKI.Red x y

      The normal-order reduction implemented by evalStep indeed computes a one-step reduction.

      source
      theorem Cslib.SKI.redexFree_of_no_red {x : SKI} (h : ∀ (y : SKI), ¬RedSKI.Red x y) :
      x.RedexFree
      source
      theorem Cslib.SKI.RedexFree.no_red {x : SKI} :
      x.RedexFree → ∀ (y : SKI), ¬RedSKI.Red x y
      source
      theorem Cslib.SKI.redexFree_iff {x : SKI} :
      x.RedexFree ↔ ∀ (y : SKI), ¬RedSKI.Red x y

      A term is redex free iff it has no one-step reductions.

      source
      theorem Cslib.SKI.redexFree_iff_evalStep {x : SKI} :
      x.RedexFree ↔ x.evalStep.isLeft = true
      source
      instance Cslib.SKI.instDecidablePredRedexFree :
      DecidablePred RedexFree
      Equations
      source
      theorem Cslib.SKI.redexFree_iff_mred_eq {x : SKI} :
      x.RedexFree ↔ ∀ (y : SKI), RedSKI.MRed x y ↔ x = y

      A term is redex free iff its only many-step reduction is itself.

      source
      theorem Cslib.SKI.commonReduct_redexFree {x y : SKI} (hy : y.RedexFree) (h : x.CommonReduct y) :
      RedSKI.MRed x y

      If a term has a common reduct with a normal term, it in fact reduces to that term.

      source
      theorem Cslib.SKI.confluent_redexFree {x y z : SKI} (hxy : RedSKI.MRed x y) (hxz : RedSKI.MRed x z) (hz : z.RedexFree) :
      RedSKI.MRed y z

      If x reduces to both y and z, and z is not reducible, then y reduces to z.

      source
      theorem Cslib.SKI.unique_normal_form {x y z : SKI} (hxy : RedSKI.MRed x y) (hxz : RedSKI.MRed x z) (hy : y.RedexFree) (hz : z.RedexFree) :
      y = z

      If x reduces to both y and z, and both y and z are in normal form, then they are equal.

      source
      theorem Cslib.SKI.eq_of_commonReduct_redexFree {x y : SKI} (h : x.CommonReduct y) (hx : x.RedexFree) (hy : y.RedexFree) :
      x = y

      If x and y are normal and have a common reduct, then they are equal.

      Injectivity for datatypes #

      source
      theorem Cslib.SKI.sk_nequiv :
      ¬S.CommonReduct K
      source
      theorem Cslib.SKI.isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool v y) (hxy : x.CommonReduct y) :
      u = v

      Injectivity for booleans.

      source
      theorem Cslib.SKI.TF_nequiv :
      ¬TT.CommonReduct FF
      source
      def Cslib.SKI.churchK :
      ℕ → SKI

      A specialisation of Church : Nat → SKI.

      Equations
      Instances For
        source
        theorem Cslib.SKI.churchK_church (n : ℕ) :
        churchK n = Church n K K
        source
        theorem Cslib.SKI.churchK_redexFree (n : ℕ) :
        (churchK n).RedexFree
        source
        @[simp]
        theorem Cslib.SKI.churchK_size (n : ℕ) :
        (churchK n).size = n + 1
        source
        theorem Cslib.SKI.churchK_injective :
        Function.Injective churchK
        source
        theorem Cslib.SKI.isChurch_injective (x y : SKI) (n m : ℕ) (hx : IsChurch n x) (hy : IsChurch m y) (hxy : x.CommonReduct y) :
        n = m

        Injectivity for Church numerals

        source
        theorem Cslib.SKI.rice {P : SKI} (hP : ∀ (x : SKI), RedSKI.MRed (P.app x) TT ∨ RedSKI.MRed (P.app x) FF) (hxt : ∃ (x : SKI), RedSKI.MRed (P.app x) TT) (hxf : ∃ (x : SKI), RedSKI.MRed (P.app x) FF) :
        False

        Rice's theorem: no SKI term is a non-trivial predicate.

        More specifically, say a term P is a predicate if, for every term x, P · x reduces to either TT or FF. A predicate P is trivial if either it always reduces to true, or always to false. This version of Rice's theorem derives a contradiction from the existence of a predicate P and the existence of terms x for which P · x is true (P · x ↠ TT) and for which P · x is false (P · x ↠ FF).

        source
        theorem Cslib.SKI.rice' {P : SKI} (hP : ∀ (x : SKI), RedSKI.MRed (P.app x) TT ∨ RedSKI.MRed (P.app x) FF) :
        (∀ (x : SKI), RedSKI.MRed (P.app x) TT) ∨ ∀ (x : SKI), RedSKI.MRed (P.app x) FF

        Rice's theorem: any SKI predicate is trivial.

        This version of Rice's theorem proves (classically) that any SKI predicate P either is constantly true (ie P · x ↠ TT for every x) or is constantly false (P · x ↠ FF for every x).