Documentation

PartialCombinatoryAlgebras.PartialCombinatoryAlgebra

Partial combinatory algebras #

A partial combinatory algebra is a set equipped with a partial binary operation, which has the so-called combinators K and S. We formalize it in two stages.

We first define the class PartialApplication which equips a given set A with a partial binary operation. One might expect such an operation to have type A → A → Part A, but this leads to complications because it is not composable. So instead we specify that a partial operation is a map of type Part A → Part A → Part A. In other words, we always work with partial elements, and separately state that they are total as necessary.

(It would be natural to require that the applications be strict, i.e., if the result is defined so are its arguments. An early version did so, but the assumption of strictness was never used.)

We then define the class PCA (partial combinatory algebra) to be an extension of PartialApplication. It prescribed combinators K and S satisfying the usual properties. Following our strategy, K and S are again partial elements on the carrier set, with a separate claim that they are total.

class PCA (A : Type u_1) extends PartialApplication A :
Type u_1

The partial combinatory structure on a set A.

Instances
    instance PCA.inhabited {A : Type u_1} [PCA A] :

    Every PCA is inhabited. We pick K as its default element.

    Equations
    • PCA.inhabited = { default := PCA.K.get }

    Expr Γ A is the type of expressions built inductively from constants K and S, variables in Γ (the variable context), the elements of a carrier set A, and formal binary application.

    The usual accounts of PCAs typically do not introduce `K` and `S`
    as separate constants, because a PCA `A` already contains such combinators.
    However, as we defined the combinators to be partial elements, it is more
    convenient to have separate primitive constants denoting them.
    Also, this way `A` need not be an applicative structure.
    
    inductive PCA.Expr (Γ : Type u_1) (A : Type u_2) :
    Type (max u_1 u_2)

    Expressions with variables from context Γ and elements from A.

    • K: {Γ : Type u_1} → {A : Type u_2} → PCA.Expr Γ A

      Formal expression denoting the K combinator

    • S: {Γ : Type u_1} → {A : Type u_2} → PCA.Expr Γ A

      Formal expression denoting the S combinator

    • elm: {Γ : Type u_1} → {A : Type u_2} → APCA.Expr Γ A

      An element as a formal expression

    • var: {Γ : Type u_1} → {A : Type u_2} → ΓPCA.Expr Γ A

      A variable as a formal expression

    • app: {Γ : Type u_1} → {A : Type u_2} → PCA.Expr Γ APCA.Expr Γ APCA.Expr Γ A

      Formal expression application

    Instances For
      instance PCA.Expr.hasDot {Γ : Type u_1} {A : Type u_2} :

      Formal application as a binary operation ·

      Equations
      • PCA.Expr.hasDot = { dot := PCA.Expr.app }
      @[reducible]
      def PCA.override {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) (a : A) (η : ΓA) (y : Γ) :
      A

      A valuation η : Γ → A assigning elements to variables, with the value of x overridden to be a.

      Equations
      Instances For
        def PCA.eval {Γ : Type u} {A : Type v} [PCA A] (η : ΓA) :
        PCA.Expr Γ APart A

        Evaluate an expression with respect to a given valuation η.

        Equations
        Instances For
          def PCA.defined {Γ : Type u} {A : Type v} [PCA A] (e : PCA.Expr Γ A) :

          An expression is said to be defined when it is defined at every valuation.

          Equations
          Instances For
            def PCA.subst {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) (a : A) :
            PCA.Expr Γ APCA.Expr Γ A

            The substitution of an element for the extra variable.

            Equations
            Instances For
              def PCA.abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) :
              PCA.Expr Γ APCA.Expr Γ A

              abstr e is an expression with one fewer variables than the expression e, which works similarly to function abastraction in the λ-calculus. It is at the heart of combinatory completeness.

              Equations
              Instances For
                @[simp]
                theorem PCA.df_abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (x : Γ) (e : PCA.Expr Γ A) :

                An abstraction is defined.

                theorem PCA.eval_abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (x : Γ) (e : PCA.Expr Γ A) (a : A) (η : ΓA) :

                eval_abstr e behaves like abstraction in the extra variable. This is known as combinatory completeness.

                theorem PCA.eval_abstr_app {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (η : ΓA) (x : Γ) (e : PCA.Expr Γ A) (u : Part A) (hu : u ) :
                PCA.eval η (PCA.abstr x e) u = PCA.eval (PCA.override x (u.get hu) η) e

                Like eval_abstr but with the application on the outside of eval.

                @[simp]
                theorem PCA.eval_override {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (η : ΓA) (x : Γ) (a : A) (e : PCA.Expr Γ A) :
                PCA.eval (PCA.override x a η) e = PCA.eval η (PCA.subst x a e)
                def PCA.compile {Γ : Type u} {A : Type v} [PCA A] (e : PCA.Expr Γ A) :

                Compile an expression to a partial element, substituting the default value for any variables occurring in e.

                Equations
                Instances For
                  def PCA.eval_closed {Γ : Type u} {A : Type v} [PCA A] :
                  PCA.Expr Γ AΓ Part A

                  Evaluate an expression under the assumption that it is closed. Return inl x if variable x is encountered, otherwise inr u where u is the partial element so obtained.

                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For