« Home

Schönfinkel's combinator calculus (Algebraic Theories) [ag-0003]

     
    {-# OPTIONS --safe --without-K #-}
module ag-0003 where

open import MLTT.Spartan

    Combinator calculus 可以看成一個代數理論，這時候它有

    1. 一個 sort of terms
    2. 一個 binary
    3. 兩個 nullary operations
    4. 兩個等式
    record combinator-calculus : 𝓤₁ ̇ where
  field
    Tm : 𝓤₀ ̇

    _·_ : Tm → Tm → Tm

    K : Tm
    S : Tm

    Kβ : {u f : Tm} → K · u · f ＝ u
    Sβ : {f g u : Tm} → S · f · g · u ＝ f · u · (g · u)

  infixl 30 _·_
    1. 從這個符號可以明顯看出代數/模型的概念
    2. Combinator calculus 的 quotiented syntax 是初始模型，它總是存在。
    3. Notions of homomorphism, displayed/dependent model, induction, products and coproducts of models, free models, and so on, are derivable from the signature, as described in any book on universal algebra
    4. Algebraic Theory 的 initial algebra 叫做 quotient inductive type

    其他 single-sorted algebraic theories 著名案例：

    1. 邏輯：經典（或直覺主義）命題邏輯，定義為布林代數（或海廷代數）理論
    2. 代數：monoids、群、環、lattices 等等