SKS system church booleans
I've been studying the SKS deep inference system. It has been a subject of the few previous posts. Right now I am examining the atomic cut elimination Kai Brünnler has presented in his paper. How does its computational meaning compare to what we have today with lambda calculus and simple types?
In Curry-Howard-based type theory,
the lambda calculus is treated as an encoding for natural deduction proofs.
The types are formulas in those proofs.
Implication elimination rule forms the computational part.
Cut elimination allows us to rewrite (+ 1 2) to 3 in lambda calculus.
I assume the computational content still stays about the same, so I thought about writing Church encoding of boolean operations for SKS system. Instead of lambda calculus you can use the proofs themselves. I will show all of that in a moment. The approach has resemblance to that from the previous week's post.
Church encoding provides primitive way to represent values in untyped lambda calculus. It is not usually used in practical implementations, but it ought to give us useful insight for how the computational content in SKS system corresponds to lambda calculus.
In the Church encoding the 'true' and 'false' are represented with the following programs:
true = λa.λb.afalse = λa.λb.b
Both of these clauses correspond to natural deduction proofs:
------ implication introductiona -> a----------- weakeninga -> b -> a
The implication introduction is a simple axiom stating that if we can get a proof for 'a', then we can prove 'a'. Weakening adds and says that if we can already prove something, then it doesn't harm if we additionally get some other proof 'b' along it.
The Church encoding uses the option to discard either value for representing booleans.
The and boolean connective is represented in the following way:
and = λp.λq.p q pThe natural deduction proof for this is more complicated because
the proposition behind 'p' variable must be passed into itself.
This means that the p = (q -> p -> r) is a recursive formula.
I can verify this by retrieving the type for the corresponding clause from Haskell's interactive evaluation prompt.
Prelude> :t \p -> \q -> p q p<interactive>:1:17:Occurs check: cannot construct the infinite type:r2 ~ r1 -> r2 -> rRelevant bindings includeq :: r1 (bound at <interactive>:1:8)p :: r1 -> r2 -> r (bound at <interactive>:1:2)In the second argument of ‘p’, namely ‘p’In the expression: p q p
Simply typed lambda calculus rejects this form of encoding for the booleans. There seems to exist an alternative encoding that can be typed:
and = λx.λy.λt.λf.x (y t f) fand :: (a -> b -> d) -> (c -> b -> a) -> c -> b -> d
The corresponding natural deduction proof can be directly read from the lambda calculus expression.
-------------------------------- implication introductionsabd, cba, c, b -> abd, cba, c, b----------------------------------- implication elimination (cba to a)abd, cba, c, b -> abd, cba, c, b, a-------------------------------------- implication elimination (abd to d)abd, cba, c, b -> abd, cba, c, b, a, d-------------------------------------- move terms aroundabd -> cba -> cbd--------------------------------------------- expand shorthands(a -> b -> d) -> (c -> b -> a) -> c -> b -> d
The correspondence is 1:1 and isomorphic. With a different method of illustration it'd be more clear. You can still see that the implication elimination, or cut rule, corresponds to the application expression in the lambda calculus.
Cut elimination is simple to present in a natural deduction system. It corresponds to the β-reduction in lambda calculus.
and true false---------------------------------------------(λx.λy.λt.λf.x (y t f) f) (λa.λb.a) (λa.λb.b)---------------------------------------------(λy.λt.λf.(λa.λb.a) (y t f) f) (λa.λb.b)----------------------------------------λt.λf.(λa.λb.a) ((λa.λb.b) t f) f---------------------------------λt.λf.(λb.((λa.λb.b) t f)) f----------------------------λt.λf.(λa.λb.b) t f-------------------λt.λf.(λb.b) f--------------λt.λf.fλt.λf.f = false
Above we used the application to glue the and -connection and
true, false together.
After that the sequence of β-reduction rules were applied to
retrieve the result that is false.
Similar results could have been obtained in a natural deduction system
with well-formed cut elimination rule.
Since types are propositions or formulas in natural deduction, they can be very specific to the point that they describe the result you must get from the function. Often the correspondence is not used in a such way that this would be obvious, but it is possible to do so.
The Curry-Howard correspondence has had massive impact to the development of all programming languages. It is even useful for studying languages that were not originally founded to the intuitionistic type theory which built over the correspondence.
The cut elimination in SKS system is not as straightforward as it is in the simply typed lambda calculus through the use of β-reduction.
When we take the Church booleans to SKS system, some complications arise that are similar to the problems of expressing the 'and' -rule.
The 'true' and 'false' can be expressed like it was expressed with the natural deduction, we just don't have lambda calculus to encode the proofs so we need to represent them graphically, at least for now.
true ::f t- w↓ ----- i↓a ∨ b ∨ ca,b : ¬Ac : Afalse ::f t- w↓ ----- i↓b ∨ a ∨ ca,b : ¬Ac : A
I am not the certain of the proof for the 'and' here. For now I am interested about what the application of the atomic cut elimination is doing there.
and ::--------- ------- --------- ------- ------- i↓(a ∨ g.d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------- sa ∨ b ∨ g.d ∧ (i ∨ d) ∧ h.e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- c↑a ∨ b ∨ g ∧ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- sa ∨ b ∨ g ∧ h ∧ (i ∨ d) ∧ e ∧ (f ∨ c) ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ d ∧ e ∧ (f ∨ c) ∨ g ∧ h ∧ i ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ g ∧ h ∧ i ∨ d ∧ e ∧ f--------------------------------------------------- c↓a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ g ∧ h ∧ ia, b, f, i : ¬Ac, d, e, g, h : A
The notation is sligthly different here, due to the differences of the SKS system. Deep inference is very sensitive to the occurrences of formulas.
Just like before, to produce a value, we got to glue everything together with a cut rule and then carry out the computation.
and true false ::--------- ------- --------- ------- ------- i↓(a ∨ g.d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------- sa ∨ b ∨ g.d ∧ (i ∨ d) ∧ h.e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- c↑a ∨ b ∨ g ∧ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- sa ∨ b ∨ g ∧ h ∧ (i ∨ d) ∧ e ∧ (f ∨ c) ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ d ∧ e ∧ (f ∨ c) ∨ g ∧ h ∧ i ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ g ∧ h ∧ i ∨ d ∧ e ∧ f f t f t--------------------------------------------------- c↓ - w↓ ----- i↓ - w↓ ----- i↓(a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ g ∧ h ∧ i) ∧ (j ∨ k ∨ l) ∧ (m ∨ n ∨ o)--------------------------------------------------------------------------------------------- i↑(a ∨ b ∨ c ∨ g ∧ h ∧ i) ∧ (m ∨ n ∨ o)--------------------------------------------------------------------------------------------- i↑a ∨ b ∨ c
Next we should carefully apply the rules of the atomic cut elimination here.
We can rewrite the c↑ in the expression away using the following rule:
S{A}-------- c↑S{A ∧ A}~~>----------------- i↓S{A ∧ (A ∧ A ∨ ¬A ∨ ¬A)}------------------------ sS{A ∧ A ∨ A ∧ (¬A ∨ ¬A)}------------------------ c↓S{A ∧ A ∨ A ∧ ¬A}------- i↑S{A ∧ A}
Similarly the co-weakening can be rewritten away:
S{A}---- w↑S{t}~~>------- i↓S{A ∧ (t ∨ f)}-------------- sS{t ∨ (A ∧ f)}-- w↓S{t ∨ (A ∧ ¬A)}-------- i↑S{t}
We have two c↑ -rules in the proof of 'and',
so that needs to be taken care of.
After it has been processed, we end up with:
and true false ::--------- ----------------- ------- --------- ----------------- ------- ------- i↓(a ∨ g.d) ∧ (g ∧ d ∨ ¬g ∨ ¬d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (h ∧ e ∨ ¬h ∨ ¬e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- sa ∨ b ∨ (g ∧ d ∨ g.d ∧ (¬g ∨ ¬d)) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ (¬h ∨ ¬e)) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- c↓a ∨ b ∨ (g ∧ d ∨ g.d ∧ ¬g.d) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ ¬h.e) ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------------------------------------- i↑a ∨ b ∨ g ∧ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- sa ∨ b ∨ g ∧ h ∧ (i ∨ d) ∧ e ∧ (f ∨ c) ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ d ∧ e ∧ (f ∨ c) ∨ g ∧ h ∧ i ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ g ∧ h ∧ i ∨ d ∧ e ∧ f f t f t--------------------------------------------------- c↓ - w↓ ----- i↓ - w↓ ----- i↓(a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ g ∧ h ∧ i) ∧ (j ∨ k ∨ l) ∧ (m ∨ n ∨ o)--------------------------------------------------------------------------------------------- i↑(a ∨ b ∨ c ∨ g ∧ h ∧ i) ∧ (m ∨ n ∨ o)--------------------------------------------------------------------------------------------- i↑a ∨ b ∨ c
The next step would be to convert the bottommost i↑ into a group of atomic rules.
The cut elimination involves partitioning ai↑ to obtain R{a}, R{¬a},
then finally R{R{f}} and contract it down to R{f}, then glue it back to the clause.
The first things happen in the bottom of the proof.
(g ∧ h ∧ i) ∧ (m ∨ n ∨ o)------------------------- i↑ ∨ (a ∨ b ∨ c)
The i↑ transforms into atomic identity.
(g ∧ h ∧ i) ∧ (m ∨ n ∨ o)------------------------- s(h ∧ i) ∧ (g ∧ m ∨ n ∨ o)------------------------- s ∨ (a ∨ b ∨ c)i ∧ (g ∧ m ∨ h ∧ n ∨ o)--------------------------- sg ∧ m ∨ h ∧ n ∨ i ∧ o----- i↑ ----- i↑ ----- i↑
We have to produce R{g} and R{m}.
R{} = a ∨ b ∨ c ∨ {}R{g}:- w↓ ----- i↓(g ∧ h ∧ i) ∧ (* ∨ n ∨ o)---------------------------- s(h ∧ i) ∧ (g ∧ * ∨ n ∨ o)------------------------- s ∨ (a ∨ b ∨ c)i ∧ (g ∧ * ∨ h ∧ n ∨ o)--------------------------- sg ∧ * ∨ h ∧ n ∨ i ∧ oR{m}:-- w↓ ------ i↓T∧ ¬g ∧ d ∨ ¬d--------- ----------------- ------- --------- ----------------- ------- ------- i↓(a ∨ g.d) ∧ (* ∧ d ∨ ¬g ∨ ¬d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (h ∧ e ∨ ¬h ∨ ¬e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- sa ∨ b ∨ (* ∧ d ∨ g.d ∧ (¬g ∨ ¬d)) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ (¬h ∨ ¬e)) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- c↓a ∨ b ∨ (* ∧ d ∨ g.d ∧ ¬g.d) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ ¬h.e) ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------------------------------------- i↑a ∨ b ∨ * ∧ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- sa ∨ b ∨ * ∧ h ∧ (i ∨ d) ∧ e ∧ (f ∨ c) ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ d ∧ e ∧ (f ∨ c) ∨ * ∧ h ∧ i ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ * ∧ h ∧ i ∨ d ∧ e ∧ f f t f t--------------------------------------------------- c↓ - w↓ ----- i↓ - w↓ ----- i↓(a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ * ∧ h ∧ i) ∧ (j ∨ k ∨ l) ∧ (m ∨ n ∨ o)(* ∧ h ∧ i) ∧ (m ∨ n ∨ o)------------------------- s(h ∧ i) ∧ (* ∧ m ∨ n ∨ o)------------------------- s ∨ (a ∨ b ∨ c)i ∧ (* ∧ m ∨ h ∧ n ∨ o)--------------------------- s* ∧ m ∨ h ∧ n ∨ i ∧ o
We treat the item as a bottom-most reduction, so the R{} stays small.
and true false ::R{m}--------------- ss↓(a ∨ b ∨ c) ∨ m------ i↓* ∨ m ∧ d ∨ ¬d--------- ---------------s- ------- --------- ----------------- ------- ------- i↓(a ∨ g.d) ∧ (* ∧ d ∨ m ∨ ¬d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (h ∧ e ∨ ¬h ∨ ¬e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- sa ∨ b ∨ (* ∧ d ∨ g.d ∧ ( m ∨ ¬d)) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ (¬h ∨ ¬e)) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- c↓a ∨ b ∨ (* ∧ d ∨ g.d ∧ ¬g.d) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ ¬h.e) ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------------------------------------- i↑a ∨ b ∨ * ∧ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- sa ∨ b ∨ * ∧ h ∧ (i ∨ d) ∧ e ∧ (f ∨ c) ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ d ∧ e ∧ (f ∨ c) ∨ * ∧ h ∧ i ∨ d ∧ e ∧ f----------------------------------------------------- sa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ * ∧ h ∧ i ∨ d ∧ e ∧ f f t--------------------------------------------------- c↓ - w↓ ----- i↓(a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ * ∧ h ∧ i) ∧ (j ∨ k ∨ l)----- i↓(a ∨ b ∨ c) ∧ h ∧ i) ∨ n ∨ o)------------------------------- s(h ∧ i) ∧ ((a ∨ b ∨ c) ∨ n ∨ o)------------------------------- si ∧ ((a ∨ b ∨ c) ∨ h ∧ n ∨ o)------------------------------- s(a ∨ b ∨ c) ∨ (h ∧ n) ∨ (i ∧ o)------- ------- i↑a ∨ b ∨ c ∨ a ∨ b ∨ c--------------------- c↓a ∨ b ∨ c
I have some ways to simplify the result, but despite those it still ends up being a very complicated proof.
-- w↓ ------ i↓T∧ ¬g ∧ d ∨ ¬d--------- ----------------- ------- --------- ----------------- ------- ------- i↓(a ∨ g.d) ∧ ( d ∨ ¬g ∨ ¬d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (h ∧ e ∨ ¬h ∨ ¬e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- sa ∨ b ∨ ( d ∨ g.d ∧ (¬g ∨ ¬d)) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ (¬h ∨ ¬e)) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- c↓a ∨ b ∨ ( d ∨ g.d ∧ ¬g.d) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ ¬h.e) ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------------------------------------- i↑a ∨ b ∨ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- ssa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ h ∧ i ∨ d ∧ e ∧ f f t t--------------------------------------------------- c↓ - w↓ ----- i↓ ----- i↓(a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ h ∧ i) ∧ (j ∨ k ∨ l) ∧ (n ∨ o)( h ∧ i) ∧ (m ∨ n ∨ o)------------------------- si ∧ ( ∨ h ∧ n ∨ o) f--------------------------- s - w↓∨ h ∧ n ∨ i ∧ o ∨ m ∨ (a ∨ b ∨ c)----- i↑ -----i↑R{m}--------------- ss↓(a ∨ b ∨ c) ∨ m------ i↓(a ∨ b ∨ c) ∨ m ∧ d ∨ ¬d--------- -------------------------s- ------- --------- ----------------- ------- ------- i↓(a ∨ g.d) ∧ ((a ∨ b ∨ c) ∧ d ∨ m ∨ ¬d) ∧ (i ∨ d) ∧ (b ∨ h.e) ∧ (h ∧ e ∨ ¬h ∨ ¬e) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- sa ∨ b ∨ ((a ∨ b ∨ c) ∧ d ∨ g.d ∧ ( m ∨ ¬d)) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ (¬h ∨ ¬e)) ∧ (f ∨ e) ∧ (f ∨ c)--------------------------------------------------------------------------------------------- c↓a ∨ b ∨ ((a ∨ b ∨ c) ∧ d ∨ g.d ∧ ¬g.d) ∧ (i ∨ d) ∧ (h ∧ e ∨ h.e ∧ ¬h.e) ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------------------------------------- i↑a ∨ b ∨ (a ∨ b ∨ c) ∧ h ∧ (i ∨ d) ∧ d ∧ e ∧ (f ∨ e) ∧ (f ∨ c)----------------------------------------------------- ssa ∨ b ∨ c ∨ d ∧ e ∧ f ∨ (a ∨ b ∨ c) ∧ h ∧ i ∨ d ∧ e ∧ f f t--------------------------------------------------- c↓ - w↓ ----- i↓(a ∨ b ∨ c ∨ d ∧ e ∧ f ∨ (a ∨ b ∨ c) ∧ h ∧ i) ∧ (j ∨ k ∨ l)----- i↓(a ∨ b ∨ c) ∧ h ∧ i) ∨ n ∨ o)------------------------------- s(h ∧ i) ∧ ((a ∨ b ∨ c) ∨ n ∨ o)------------------------------- si ∧ ((a ∨ b ∨ c) ∨ h ∧ n ∨ o)------------------------------- s(a ∨ b ∨ c) ∨ (h ∧ n) ∨ (i ∧ o)------- ------- i↑a ∨ b ∨ c ∨ a ∨ b ∨ c--------------------- c↓a ∨ b ∨ c
Just the first cut-elimination step caused the proof to grow into this size. The next step would further cause it to grow. It looks like I may need a different cut elimination algorithm to finish this study.