Lambek Encoding

Categorical Semantics of Inductive Encodings

Initial Object

let I = data List: (A:*) -> * := (nil: () -> List A) (cons: A -> List A -> List A)

Representing Functor F

FA = 1 + A * X

Construct corresponding F-Algebra

record ListAlg: (A:*) -> * := (X: *) (nil: () -> X) (cons: A -> X -> X)

Introduce List Morphisms

infix '=' := Setoid.Ob.Equ record ListMor: (A: *) -> (x1 x2: ListAlg A) -> * := (map: x1.X -> x2.X) (okNil: Eq (map x1.nil) x2.nil) (okCons: ∀ (a: A) -> ∀ (x: x1) -> map x1.cons a x = x2.cons a (map x))

Introduce connected points of List type

record ListPoint: (A: *) -> * := (point: ∀ (x: ListAlg A) -> x.X) (pointOk: ∀ (x1 x2: ListAlg A) -> ∀ (m: ListMor A x1 x2) -> Setoid.Ob.Equ (map m point x1) (point x2))

Theorem

def ⓪ := Cat.mk () def ① := Cat.mk 𝟙ListAlg record Theorem := * (intro: colim ⓪ = lim ①)
$$ \require{AMSmath} \require{AMSsymbols} \def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$
$$U = ListAlg\\$$ $$U\ I = lim\ U\\$$ $\begin{array}{c}lim\ U\\\mapdown{\pi_i}\\X_i\end{array} \Longrightarrow \begin{array}{c}F\ lim\ U\\\mapdown{F\ \pi_i}\\F\ X_i\end{array} \Longrightarrow lim\ \begin{array}{c}F\ lim\ U\\\mapdown{F \pi_i}\\F\ X_i\end{array}$

Precise Encoding

Our encoding allows you to precise control the type of encoded parameter. There is only three cases and three equations: 1) for unit; 2) particular functorial type over a parameter type and 3) recursive embedding such as in Cons constructor.

q — is a limit in Dialg P category. The constructor body is calculated with q applied to forgetful functor U.

$$ q_{P,D,G} : End\ P\ (G'(-),G'(-)) \rightarrow P\ (Lim\ G',Lim\ G') \\ P : Set° \times Set \rightarrow Set \\ U : Dialg\ P \rightarrow Set \\ G : D \rightarrow Dialg\ P \\ G' = UG : D \rightarrow Set \\ U (Lim\ G) = Lim\ G' $$

Unit Parameters

Like for Bool or Nil constructors encoding.

$$ P_0(A,B) = B \\ q_0\ e : Lim\ G' \\ q_0\ e = e $$

Fixed Type Parameters

Like for Cons first parameter.

$$ P_1(A,B) = X \rightarrow P(A,B) \\ q_1\ e : X \rightarrow P ( Lim\ G', Lim\ G' ) \\ q_1\ e\ x\ A = e\ A\ x $$

Recursive Parameters

Like for Cons second parameter. This case is a key in encoding recursive data types such as Lists and recursive record types such as Streams.

$$ P_2(A,B) = A \rightarrow P(A,B) \\ q_2\ e : Lim\ G' \rightarrow P ( Lim\ G', Lim\ G' ) \\ q_2\ e\ I\ A = e\ A\ (I\ A) $$

Identity Functor Encoding

As known as predicative encoding

$$ \begin{array}{ccccccc} A & & \mapright{f} & & B & \mapright{f} & Set \\[3pt] & \mapdiagl{a} & \varphi & \mapdiagr{b} & & \searrow & \mapdown{\mathbf{1}} \\ & & Set & & & & Set \end{array} $$
$\varphi : a \rightarrow b$

Identity Functor Limit Encoding

As known as impredicative encoding

$$ \begin{array}{ccccccc} A & & \mapright{f} & & B & \mapright{f} & Set \\[3pt] & \mapdiagl{a} & \varphi & \mapdiagr{b} & & \searrow & \mapdown{\mathbf{1}} \\ & & Set & & & & Set \end{array} $$
$lim\ \varphi : lim\ a \rightarrow lim\ b$

Resources

  1. Om archives.
  2. Inf archives.
  3. Git sources.
  4. Inf git sources.