Deep inference combinators

Kai Brünnler and Richard McKinley described deep inference combinators in their paper "An Algorithmic Interpretation of a Deep Inference System".

xkapastel introduced me to these combinators and I think they deserve a closer examination.

It is this system from the previous week:

  A
----- c
A ∧ A

A ∧ B
----- w1
  A

A ∧ B
----- w2
  B

     B
----------- i
A ⊃ (B ∧ A)

(A ⊃ B) ∧ A
----------- e
     B

The formulas are defined as expressions consisting of variables, conjunction and implication.

A ::= a | (A ∧ A) | (A ⊃ A)

The deep inference derivations are captured by proof terms, they are defined with the following grammar:

R ::= id | p | (R . R) | (R ∧ R) | (R ⊃ R)

'id' is an identity.
'p' is a name of the inference rule from the system.

Here are the reduction rules. The paper describes them in a neat graphical syntax, but for my examination I'm going to need them as rewrite rules.

nc:  R . c ├ c . R ∧ R
nw1: R ∧ T . w1 ├ w1 . R
nw2: R ∧ T . w2 ├ w2 . T
β∧1: c . w1 ├ id
β∧2: c . w2 ├ id
ni: R . i ├ i . id ⊃ R ∧ id
β⊃: (i . (id ⊃ R)) ∧ T . e ├ id ∧ T . R

Also supplying the graphical representation of the rules:

R . c
--------- nc
c . R ∧ R

R ∧ T . w1
---------- nw 1
w1 . R

R ∧ T . w2
---------- nw 2
w2 . T

c . w1
------ β∧
id

c . w2
------ β∧
id

R . i
--------------- ni
i . id ⊃ R ∧ id

(i . (id ⊃ R)) ∧ T . e
---------------------- β⊃
id ∧ T . R

We are able to do encode church booleans in this system:

true  = i . id ⊃ (w2 . w1)
false = i . id ⊃ (w2 . w2)
and = i . id ⊃ (w2 . c . w2 ^ id . e)

Here's an evaluation to show how the and ^ (true ^ true) . e is reduced:

(i . id ⊃ (w2 . c . w2 ^ id . e)) ∧ ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))) . e
------------------------------------------------------------------------------------- β⊃
id ∧ ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))) . w2 . c . w2 ^ id . e
--------------------------------------------------------------------------- nw 2
w2 . (i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1)) . c . w2 ^ id . e
--------------------------------------------------------------------------- nc
w2 . c . ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))) ∧
    ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))) . w2 ^ id . e
---------------------------------------------------------------
w2 . c . ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1)) . w2) ∧
    ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1)) . id) . e
---------------------------------------------------------- nw 2 & id
w2 . c . (w2 . (i . id ⊃ (w2 . w1))) ∧
    (id . (i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))) . e
----------------------------------------------------------
w2 . c . w2 ∧ id .
  ((i . id ⊃ (w2 . w1))) ∧
  (id . (i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))) . e
---------------------------------------------------------- β⊃
w2 . c . w2 ∧ id .
  id ∧ ((i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1)))
  . w2 . w1
--------------------------------------------------------- nw 2
w2 . c . w2 ∧ id . w2 .
  (i . id ⊃ (w2 . w1)) ∧ (i . id ⊃ (w2 . w1))
  . w1
--------------------------------------------------------- nw 1
w2 . c . w2 ∧ id . w2 . w1 . i . id ⊃ (w2 . w1)

The reduction leaves a trail of c, id, w1, w2 combinators behind it. Since the left side of the original expression is a ∧ (a ∧ x), we could reason there should be c . id ∧ c preceding the expression. If we add those missing combinators, we will get the following further reductions:

c . id ∧ c . w2 . c . w2 ∧ id . w2 . w1 . i . id ⊃ (w2 . w1)
------------------------------------------------------------ nw 2
c . w2 . c . c . w2 ∧ id . w2 . w1 . i . id ⊃ (w2 . w1)
------------------------------------------------------------ β∧
c . c . w2 ∧ id . w2 . w1 . i . id ⊃ (w2 . w1)
------------------------------------------------------------ nw 2
c . c . w2 . w1 . i . id ⊃ (w2 . w1)
------------------------------------------------------------ β∧
c . w1 . i . id ⊃ (w2 . w1)
------------------------------------------------------------ β∧
i . id ⊃ (w2 . w1)

Our fragment of church booleans would appear to be working there. Lets still verify this by doing it with true ∧ true replaced by abstract variables.

c . id ∧ c . (i . id ⊃ (w2 . c . w2 ^ id . e)) ∧ (a ∧ b) . e
------------------------------------------------------------ β⊃
c . id ∧ c . id ∧ (a ∧ b) . w2 . c . w2 ^ id . e
------------------------------------------------
c . id ∧ (c . a ∧ b) . w2 . c . w2 ^ id . e
------------------------------------------- nw 2
c . w2 . c . a ∧ b . c . w2 ^ id . e
------------------------------------ β∧
c . a ∧ b . c . w2 ^ id . e
--------------------------------------- nc
c . c . (a ∧ b) ∧ (a ∧ b) . w2 ^ id . e
---------------------------------------
c . c . (a ∧ b . w2) ∧ (a ∧ b) . e
---------------------------------- nw 2
c . c . (w2 . b) ∧ (a ∧ b) . e
---------------------------------
c . c . w2 ∧ id . b ∧ (a ∧ b) . e
------------------------------------- nc
c . c ∧ c . w2 ∧ id . b ∧ (a ∧ b) . e
-------------------------------------
c . (c . w2) ∧ c . b ∧ (a ∧ b) . e
---------------------------------- β∧
c . id ∧ c . b ∧ (a ∧ b) . e

The result corresponds to what you'd expect it to be with lambda calculus.

This system itself doesn't seem very interesting, although you can extend it with more of intuitionistic logic to make it more interesting.

Open deduction and the notation presented here seem to make the proof-encoding very easy task to do for any logic. Also the resulting proofs are easy to treat as a sort of an algebra.

Similar posts