Documentation

Cslib.Languages.CombinatoryLogic.Defs

SKI Combinatory Logic #

This file defines the syntax and operational semantics (reduction rules) of combinatory logic, using the SKI basis.

Main definitions #

Notation #

References #

The setup of SKI combinatory logic is standard, see for example:

source
🔶 coverage
inductive Cslib.SKI :
Type

An SKI expression is built from the primitive combinators S, K and I, and application.

  • S : SKI

    S-combinator, with semantics $λxyz.xz(yz)

  • K : SKI

    K-combinator, with semantics $λxy.x$

  • I : SKI

    I-combinator, with semantics $λx.x$

  • app : SKI → SKI → SKI

    Application $x y ↦ xy$

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance Cslib.instReprSKI :
    Repr SKI
    Equations
    source
    🔸 coverage
    def Cslib.instReprSKI.repr :
    SKI → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    • Cslib.instReprSKI.repr Cslib.SKI.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cslib.SKI.S")).group prec✝
    • Cslib.instReprSKI.repr Cslib.SKI.K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cslib.SKI.K")).group prec✝
    • Cslib.instReprSKI.repr Cslib.SKI.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cslib.SKI.I")).group prec✝
    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance Cslib.instDecidableEqSKI :
      DecidableEq SKI
      Equations
      source
      🔸 coverage
      def Cslib.instDecidableEqSKI.decEq (x✝ x✝¹ : SKI) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        🔸 coverage
        def Cslib.SKI.«term_⬝_» :
        Lean.TrailingParserDescr

        Application $x y ↦ xy$

        Equations
        • Cslib.SKI.«term_⬝_» = Lean.ParserDescr.trailingNode `Cslib.SKI.«term_⬝_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ ") (Lean.ParserDescr.cat `term 101))
        Instances For
          source
          🔸 coverage
          def Cslib.SKI.applyList (f : SKI) (xs : List SKI) :
          SKI

          Apply a term to a list of terms

          Equations
          Instances For
            source
            📐 coverage
            theorem Cslib.SKI.applyList_concat (f : SKI) (ys : List SKI) (z : SKI) :
            f.applyList (ys ++ [z]) = (f.applyList ys).app z
            source
            🔸 coverage
            def Cslib.SKI.size :
            SKI → ℕ

            The size of an SKI term is its number of combinators.

            Equations
            Instances For

              Reduction relations between SKI terms #

              source
              🔶 coverage
              inductive Cslib.SKI.Red :
              SKI → SKI → Prop

              Single-step reduction of SKI terms

              Instances For
                source
                🔸 coverage
                def Cslib.SKI.«term_⭢_» :
                Lean.TrailingParserDescr
                Equations
                • Cslib.SKI.«term_⭢_» = Lean.ParserDescr.trailingNode `Cslib.SKI.«term_⭢_» 1022 39 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⭢ ") (Lean.ParserDescr.cat `term 39))
                Instances For
                  source
                  🔸 coverage
                  def Cslib.SKI.«term_↠_» :
                  Lean.TrailingParserDescr
                  Equations
                  • Cslib.SKI.«term_↠_» = Lean.ParserDescr.trailingNode `Cslib.SKI.«term_↠_» 1022 39 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↠ ") (Lean.ParserDescr.cat `term 39))
                  Instances For
                    source
                    theorem Cslib.SKI.Red.ne {x y : SKI} :
                    x.Red y → x ≠ y
                    source
                    📐 coverage
                    theorem Cslib.SKI.MRed.S (x y z : SKI) :
                    Relation.ReflTransGen Red (((SKI.S.app x).app y).app z) ((x.app z).app (y.app z))
                    source
                    📐 coverage
                    theorem Cslib.SKI.MRed.K (x y : SKI) :
                    Relation.ReflTransGen Red ((SKI.K.app x).app y) x
                    source
                    📐 coverage
                    theorem Cslib.SKI.MRed.I (x : SKI) :
                    Relation.ReflTransGen Red (SKI.I.app x) x
                    source
                    📐 coverage
                    theorem Cslib.SKI.MRed.head {a a' : SKI} (b : SKI) (h : Relation.ReflTransGen Red a a') :
                    Relation.ReflTransGen Red (a.app b) (a'.app b)
                    source
                    📐 coverage
                    theorem Cslib.SKI.MRed.tail (a : SKI) {b b' : SKI} (h : Relation.ReflTransGen Red b b') :
                    Relation.ReflTransGen Red (a.app b) (a.app b')
                    source
                    📐 coverage
                    theorem Cslib.SKI.parallel_mRed {a a' b b' : SKI} (ha : Relation.ReflTransGen Red a a') (hb : Relation.ReflTransGen Red b b') :
                    Relation.ReflTransGen Red (a.app b) (a'.app b')
                    source
                    📐 coverage
                    theorem Cslib.SKI.parallel_red {a a' b b' : SKI} (ha : a.Red a') (hb : b.Red b') :
                    Relation.ReflTransGen Red (a.app b) (a'.app b')
                    source
                    📐 coverage
                    theorem Cslib.SKI.mJoin_red_head {x x' : SKI} (y : SKI) :
                    Relation.MJoin Red x x' → Relation.MJoin Red (x.app y) (x'.app y)
                    source
                    📐 coverage
                    theorem Cslib.SKI.mJoin_red_tail (x : SKI) {y y' : SKI} :
                    Relation.MJoin Red y y' → Relation.MJoin Red (x.app y) (x.app y')