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Γ⊢E:A lax means EE as a computational evidence might not terminate. It might not give me AA at the end. Think of it like a “possibility” that EE will give me AA.
{E}{E} a suspended computation of EE.
<E/x>F<E/x>F is a kind of substitution of EE for xx in FF. It is an operration on proof/computation. Will talk about it later.
So we have the following structural rules or judgemental rules about laxlax:
1.
Γ⊢M:A trueΓ⊢M:A laxΓ⊢M:A trueΓ⊢M:A lax2.
Γ⊢E:A lax,Γx:A true⊢F:C laxΓ⊢<E/x>F:C laxΓ⊢E:A lax,Γx:A true⊢F:C laxΓ⊢<E/x>F:C laxWe now introduce a new proposition ◯A◯A Monad:
Introduction rule (II):
Γ⊢E:A laxΓ⊢{E}:◯A trueΓ⊢E:A laxΓ⊢{E}:◯A trueElimination rules (EE):
Γ⊢M:◯A true,Γx:A true⊢F:C laxΓ⊢let_{x}=Min_F:C laxΓ⊢M:◯A true,Γx:A true⊢F:C laxΓ⊢let−−−{x}=Min−−F:C laxSummarize local reduction and local expansion:
let_{x}={E}in_F⟹R<E/x>Flet−−−{x}={E}in−−F⟹R<E/x>F M:◯A⟹E{let_{x}=Min_x}M:◯A⟹E{let−−−{x}=Min−−x}So because EE is type of A laxA lax, according to the second structural rules about laxlax: Γ⊢E:A lax,Γx:A true⊢F:C laxΓ⊢<E/x>F:C laxΓ⊢E:A lax,Γx:A true⊢F:C laxΓ⊢<E/x>F:C lax, it could be comming from two places:
-
The first structural rules about laxlax: Γ⊢M:A trueΓ⊢M:A laxΓ⊢M:A trueΓ⊢M:A lax. So EE is MM.
-
The elimination rules of ◯A◯A: Γ⊢M:◯A true,Γx:A true⊢F:C laxΓ⊢let_{x}=Min_F:C laxΓ⊢M:◯A true,Γx:A true⊢F:C laxΓ⊢let−−−{x}=Min−−F:C lax. (Note: Here FF and CC could be anything). So EE is let_{x}=Min_Flet−−−{x}=Min−−F
So we write: E=M|let_{x}=Min_FE=M|let−−−{x}=Min−−F
For the elimination rule case, we can see Γ⊢M:◯A trueΓ⊢M:◯A true. For something have type ◯A◯A, according to the Introduction rule of ◯A◯A, it could be that M=EM=E
Therefore, MM is everything as before plus one possibility:
We write: M=…{E}M=…{E}
Then we can define <E/x>F<E/x>F:
<E/x>F=<M/x>F=[M/x]For<let_{y}=Min_E′/x>F=let_{y}=Min_<E′/x>F<E/x>F=<M/x>F=[M/x]For<let−−−{y}=Min−−E′/x>F=let−−−{y}=Min−−<E′/x>FLet’s Write Some Proofs/ProgramsPermalink
For (A⊃(B⊃C))⊃((A∧B)⊃C)(A⊃(B⊃C))⊃((A∧B)⊃C) which is uncurrying, we have the proof: λf.λp.f(first p)(second p)λf.λp.f(first p)(second p)
For ((A∧B)⊃C)⊃(A⊃(B⊃C))((A∧B)⊃C)⊃(A⊃(B⊃C)) which is currying, we have the proof: λg.λx.λy.g<x,y>λg.λx.λy.g<x,y>
For monad in functional programming we have two requirements to satisfy:
return:A⊃◯Abind:◯A⊃(A⊃◯B)⊃◯Breturn:A⊃◯Abind:◯A⊃(A⊃◯B)⊃◯Bsuch that
bind(return z)f=fzbind(return z)f=fzTo proof returnreturn:
A⊃◯AA⊃◯Awe have:
λx.{x}λx.{x}To proof bindbind:
◯A⊃(A⊃◯B)⊃◯B◯A⊃(A⊃◯B)⊃◯Bwe have:
λx.λf.{let_{x′}=xin_ let_{y}=fx′in_ y}λx.λf.{let−−−{x′}=xin−− let−−−{y}=fx′in−− y}To proof
bind(return x)f=fxbind(return x)f=fxwe have:
(λx.λf.{let_{x′}=x in_ let_{y}=fx′ in_ y})((λx.{x})z)f={let_{x′}=(λx.{x})z in_ let_{y}=fx′ in_ y}={let_{x′}={z} in_ let_{y}=fx′ in_ y}={let_{y}=fz in_ y}=fz
Comments