Computational Interpretations

Here we will talk about computational interpretations by the example of lax logic. Hope from the example we can have sense of how logic and PL are connected.

Lax and MonandPermalink

Some notations:

Γ⊢E:A lax$\Gamma ⊢E:Alax$ means E$E$ as a computational evidence might not terminate. It might not give me A$A$ at the end. Think of it like a “possibility” that E$E$ will give me A$A$.

{E}$\left\{E\right\}$ a suspended computation of E$E$.

<E/x>F$<E/x>F$ is a kind of substitution of E$E$ for x$x$ in F$F$. It is an operration on proof/computation. Will talk about it later.

So we have the following structural rules or judgemental rules about lax$lax$:

1.

2.

We now introduce a new proposition ◯A$◯A$ Monad:

Introduction rule (I$I$):

Elimination rules (E$E$):

Summarize local reduction and local expansion:

So because E$E$ is type of A lax$Alax$, according to the second structural rules about lax$lax$: Γ⊢E:A lax,Γx:A true⊢F:C laxΓ⊢<E/x>F:C lax$\frac{\Gamma ⊢E:Alax,\Gamma x:Atrue⊢F:Clax}{\Gamma ⊢<E/x>F:Clax}$, it could be comming from two places:

1. The first structural rules about lax$lax$: Γ⊢M:A trueΓ⊢M:A lax$\frac{\Gamma ⊢M:Atrue}{\Gamma ⊢M:Alax}$. So E$E$ is M$M$.

2. The elimination rules of ◯A$◯A$: Γ⊢M:◯A true,Γx:A true⊢F:C laxΓ⊢let_{x}=Min_F:C lax$\frac{\Gamma ⊢M:◯Atrue,\Gamma x:Atrue⊢F:Clax}{\Gamma ⊢\underset{-}{let}\left\{x\right\}=M\underset{-}{in}F:Clax}$. (Note: Here F$F$ and C$C$ could be anything). So E$E$ is let_{x}=Min_F$\underset{-}{let}\left\{x\right\}=M\underset{-}{in}F$

So we write: E=M|let_{x}=Min_F$E=M|\underset{-}{let}\left\{x\right\}=M\underset{-}{in}F$

For the elimination rule case, we can see Γ⊢M:◯A true$\Gamma ⊢M:◯Atrue$. For something have type ◯A$◯A$, according to the Introduction rule of ◯A$◯A$, it could be that M=E$M=E$

Therefore, M$M$ is everything as before plus one possibility:

We write: M=…{E}$M=\dots \left\{E\right\}$

Then we can define <E/x>F$<E/x>F$:

Let’s Write Some Proofs/ProgramsPermalink

For (A⊃(B⊃C))⊃((A∧B)⊃C)$(A\supset (B\supset C\left)\right)\supset \left(\right(A\wedge B)\supset C)$ which is uncurrying, we have the proof: λf.λp.f(first p)(second p)$\lambda f.\lambda p.f\left(firstp\right)\left(secondp\right)$

For ((A∧B)⊃C)⊃(A⊃(B⊃C))$\left(\right(A\wedge B)\supset C)\supset (A\supset (B\supset C\left)\right)$ which is currying, we have the proof: λg.λx.λy.g<x,y>$\lambda g.\lambda x.\lambda y.g<x,y>$

For monad in functional programming we have two requirements to satisfy:

such that

To proof return$return$:

we have:

To proof bind$bind$:

we have:

To proof

we have: