Toward typing of the concurrent expression language

Some while ago I came up with this idea of a concurrent linear expression language. The language would use logical formulas as types, but I've been wondering how to typecheck and type inference the language.

I recently realised that I can use deep inference to derive types for expressions.

Short example

For example consider this addition:

abc(D):
    plus(1, 2; C)
    plus(C, 3; D)

We can arrive to the type by instantiating 'plus' twice and conjuncting the clauses.

a:Num. b:Num.
(¬a{1} ∨ ¬a{2} ∨ a{C}) ∧ (¬b{C} ∨ ¬b{3} ∨ b{D})

The numeric arguments already plug away some of the variables, so we can remove those as long as we remember that this constraints the polarities. I denote that with a '+' in the type variable's constraint.

This leaves us:

a:Num+. b:Num+.
a{C} ∧ (¬b{C} ∨ b{D})

Now we start applying deep inference rules as if we were trying to construct a refutation. The 's' -rule in deep inference can be applied to leave us with conjunction of C. This allows introducing a cut for connecting the C and eliminating it.

a:Num+. b:Num+.
       a{C} ∧ (¬b{C} ∨ b{D})
       --------------------- s
       a{C} ∧ ¬b{C} ∨ b{D}
       ------------------- ai↑ {a = b}
       f ∨ a{D}
---------------
a:Num+. a{D}

This is the type for abc(D).

Deep inference rules relevant for this

The language was inspired by classical linear logic. But it seems that the deep inference rules for classical logic work fine as well.

The atomic cut, switch and medial seem to form the machinery that allows type inference of these expressions.

a ∧ ¬a
------ ai↑
  f

A ∧ (B ∨ C)
----------- s
A ∧ B ∨ C

(A ∧ B) ∨ (C ∧ D)
----------------- m
(A ∨ D) ∧ (B ∨ D)

We can create few rules to introduce the additive operators from the linear logic. I think they behave like the choice-operators from Computability logic, so I use that notation here.

These are introduction rules for choice. The first one eliminates conjunctive choice. The second one introduces disjunctive choice.

A ⊓ B
----- ci↑
  A

  A
----- ci↓
A ⊔ B

How do I know these are correct? Well if we think about it with the game semantics. The disjunctive choice can be proven if we can prove the either one formula. This means that the second rule is likely right. The second rule can be inverted and we get the other rule.

I realised that we may need specific switching rules for deriving types from formulas containing additive operators.

A ∨ C ⊓ B ∨ C
------------- cs↑
(A ⊓ B) ∨ C

(A ⊔ B) ∧ C
------------- cs↓
A ∧ C ⊔ B ∧ C

Switching rules for choice move values into and away from the context introduced by additive operators.

What are these programs?

I think the actual programs are those proof derivations and the source programs represent them as their atomic flows.

Not sure about all the things the types introduce to this language, but it'd seem that the deadlocking programs are blocked away. Here's an another example of a valid clause and a clause that contains a deadlock. With their respective type derivations that show this.

a_clause(B,C,X,D):
    A = plus(B, C)
    D = plus(A, X)

(¬B ∨ ¬C ∨ A) ∧ (¬A ∨ ¬X ∨ D)
----------------------------- s
¬B ∨ ¬C ∨ (A) ∧ (¬A) ∨ ¬X ∨ D
----------------------------- ai↑
¬B ∨ ¬C ∨ f          ∨ ¬X ∨ D
-----------------------------
¬B ∨ ¬C ∨ ¬X ∨ D


b_clause(B,X):
    A = plus(B, C)
    C = plus(A, X)

(¬B ∨ ¬C ∨ A) ∧ (¬A ∨ ¬X ∨ C)
----------------------------- s
¬B ∨ (¬C ∨ A) ∧ (¬A ∨ C) ∨ ¬X
-----------------------------
Unable to cut away C and A.

It would seem that if we have two cuts, we can first find the first way to cut and then find the second from there. I'm not sure about that though.

It probably needs some kind of a way to pivot between infinite amount of proof permutations we can get. I'm not sure if it's proof focusing that I need here, or something else.

Truth tables and choice

With the choice-operators we are able to provide truth tables and conditionals into the language. I think they could be also brought in other ways, but this one is neat.

invert(y, n)
invert(n, y)

(y∨n) ⊓ (n∨y)

and(n,n,n)
and(n,y,n)
and(y,n,n)
and(y,y,y)

(n∨n∨n) ⊓ (n∨y∨n) ⊓ (y∨n∨n) ⊓ (y∨y∨y)

The apparent problem here is that the atomic flow charts are quite not enough. For example the invert clause we have here easily flexes out to a formula that'd make sense for inversion:

(y:0 ∨ n:1) ⊓ (n:0 ∨ y:1)
----------------------------------------- ci↓
(y:0 ∨ (y:1 ⊔ n:1)) ⊓ (n:0 ∨ (y:1 ⊔ n:1))
----------------------------------------- cs↑
(y:0 ⊓ n:0) ∨ (y:1 ⊔ n:1)

We can slide the choice out via an atomic cut and use this table to invert a boolean value.

What would we do if we wanted to represent implication through these tables?

implication(A,B,C):
  invert(A,NA)
  invert(C,NC)
  and(NA, B, NC)

Does it work?

((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧
((y:C ∨ n:NC) ⊓ (n:C ∨ y:NC)) ∧
(n:NA ∨ n:B ∨ n:NC) ⊓ (n:NA ∨ y:B ∨ n:NC) ⊓ (y:NA ∨ n:B ∨ n:NC) ⊓ (y:NA ∨ y:B ∨ y:NC)
-------------------------------------------------------------------------------------
((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B) ∨ n:NC) ⊓ (y:NA ∨ y:B ∨ y:NC)
--------------------------------------------------------------------------- ci↓ + cs↑
((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧
((y:C ∨ n:NC) ⊓ (n:C ∨ y:NC)) ∧
(((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B)) ⊔ (y:NA ∨ y:B) ∨ (n ⊓ y):NC)
--------------------------------------------------------------------------- ci↓ + cs↑
((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧
((y:C ⊓ n:C) ∨ (n ⊔ y):NC) ∧
(((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B)) ⊔ (y:NA ∨ y:B) ∨ (n ⊓ y):NC)
--------------------------------------------------------------------------- s
((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧
((y:C ⊓ n:C) ∨ 
 ((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B)) ⊔ (y:NA ∨ y:B) ∨
 (n ⊓ y):NC ∧ (n ⊔ y):NC)
--------------------------------------------------------------------------- ai↑
((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧
((y:C ⊓ n:C) ∨ 
 (((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B)) ⊔ (y:NA ∨ y:B))
-------------------------------------------------------------------------------------------- s
(y:C ⊓ n:C) ∨ 
((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧ (((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B)) ⊔ (y:NA ∨ y:B)
-------------------------------------------------------------------------------------------- cs↓
(y:C ⊓ n:C) ∨ 
((((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧ ((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B))) ⊔
 (((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧  (y:NA ∨ y:B)))
-------------------------------------------------------------------------------------------- ci↑
(y:C ⊓ n:C) ∨ 
((((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧ ((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B))) ⊔
 ((n:A ∨ y:NA) ∧ (y:NA ∨ y:B)))
-------------------------------------------------------------------------------------------- s + ai↑
(y:C ⊓ n:C) ∨ 
((((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧ ((n:NA ∨ n:B) ⊓ (n:NA ∨ y:B) ⊓ (y:NA ∨ n:B))) ⊔
 ((n:A ∨ y:B)))
---------------------------------------------------------------------------------
(y:C ⊓ n:C) ∨ 
((((y:A ∨ n:NA) ⊓ (n:A ∨ y:NA)) ∧ ((n:NA ∨ (n:B ⊓ y:B)) ⊓ (y:NA ∨ n:B))) ⊔
 ((n:A ∨ y:B)))
--------------------------------------------------------------------------------- ci↓ + cs↑ + s
(y:C ⊓ n:C) ∨ 
((((y:A ⊓ n:A) ∨ (n:NA ⊔ y:NA) ∧ ((n:NA ∨ (n:B ⊓ y:B)) ⊓ (y:NA ∨ n:B))) ⊔
 ((n:A ∨ y:B)))
--------------------------------------------------------------------------------- ci↓ + cs↑ + s
(y:C ⊓ n:C) ∨ 
(((y:A ⊓ n:A) ∨ (n:NA ⊔ y:NA) ∧ ((n:NA ∨ (n:B ⊓ y:B)) ⊓ (y:NA ∨ n:B))) ⊔
 ((n:A ∨ y:B)))
--------------------------------------------------------------------------------- ci↑ + ai↑
(y:C ⊓ n:C) ∨ (((y:A ⊓ n:A) ∨ ((n:B ⊓ y:B) ⊔ n:B)) ⊔ ((n:A ∨ y:B)))

It seems like we arrived to some interesting result, but what does it say? If we treat it as a game, it'd seem that there is interleaving between choices. If the formula is inverted...

(y:C ⊔ n:C) ∧ (((y:A ⊔ n:A) ∧ ((n:B ⊔ y:B) ⊓ n:B)) ⊓ ((n:A ∧ y:B)))

...and then interpreted game theoretically, it says:

  1. There are two games where we participate and have to play both.
  2. In the first game we choose the value of 'C'.
  3. In the second game the environment chooses between second and third game.
  4. If environment chooses the third game, then A is 'no' and B is 'yes'.
  5. If environment chooses the second game, then we again have to choose value for A and wait for environment to decide on the second game.
  6. Finally the value of B is either 'n', 'y' of our choice. Or then it's 'n'.

It'd seem that it has formed a game where we fight ourselves. The overall type of the clause tells less than the truth table would tell.

Lets examine the implication's truth table:

implication(y, y, y)
implication(y, n, n)
implication(n, y, y)
implication(n, n, y)

So we choose the value of 'C'. If we choose 'n', then we end up with the 'y', 'n' -case. We probably did an error somewhere and the values flipped around, but that'd seem to match the table's interpretation:

implication(y, y, y)
implication(n, y, y)
implication(n, n, y)

implication(y, n, n)

Then we have a opportunity to choose the value of A. We choose either 'yes' or 'no. And end up with.

implication(n, y, y)
implication(n, n, y)

implication(y, y, y)

It's all-yes or then we have choice between 'y' and 'n' again.

I didn't make it to work, but the result was pretty interesting. Probably ended up doing a wrong derivation somewhere and ended getting this result.

The type inference would probably need some sort of deep-inference proof search here.

It may also be that the proof search itself is the normalisation procedure that can compute these programs while also being the type inference and checking algorithm.

Similar posts