GaeBlogX Arista Networks, Software-Defined Networking

# Computational Interpretations

2018-02-18
Yanxi Chen

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 Monand

Some notations:

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

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

$% F %]]>$ is a kind of substitution of $E$ for $x$ in $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$:

1.

2.

We now introduce a new proposition $\bigcirc A$ Monad:

Introduction rule ($I$):

Elimination rules ($E$):

Summarize local reduction and local expansion:

So because $E$ is type of $A\ lax$, according to the second structural rules about $lax$: $% F:C\ lax} %]]>$, it could be comming from two places:

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

2. The elimination rules of $\bigcirc A$: $\frac{\Gamma\vdash M:\bigcirc A\ true,\Gamma x:A\ true\vdash F:C\ lax} {\Gamma\vdash \underline{let} \{x\}=M\underline{in} F:C\ lax}$. (Note: Here $F$ and $C$ could be anything). So $E$ is $\underline{let} \{x\}=M\underline{in} F$

So we write: $E=M|\underline{let} \{x\}=M\underline{in} F$

For the elimination rule case, we can see $\Gamma\vdash M:\bigcirc A\ true$. For something have type $\bigcirc A$, according to the Introduction rule of $\bigcirc A$, it could be that $M={E}$

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

We write: $M=\ldots\{E\}$

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

## Let’s Write Some Proofs/Programs

For $(A\supset(B\supset C))\supset((A\wedge B)\supset C)$ which is uncurrying, we have the proof: $\lambda f.\lambda p.f(first\ p)(second\ p)$

For $((A\wedge B)\supset C)\supset (A\supset (B\supset C))$ which is currying, we have the proof: $% %]]>$

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

such that

To proof $return$:

we have:

To proof $bind$:

we have:

To proof

we have: