Programming languages such as Vault, Rust, etc.. have recently popularized substructural logics. Their type systems share various forms of resource awareness.
Foto: Jan Łukasiewicz
Propositional substructural logics were already discussed when Jan Łukasiewicz and Carew Arthur Meredith met in 1947 in Dublin. We will investigate such logics with the help of Prolog.
Hilbert-Style Calculus
We are gonne present a couple of substructural logics as instances of the more general pattern of combinatory logics. They consists of axiom schemas indentified by polymorphic constants C_1,..,C_n and the modus ponens.
|- s : A -> B |- t : A
---------------------------- (Modus Ponens)
|- (s t) : B
-------------- (Axiom Schema i)
|- C_i : A_i
Combinatory logics are the Curry-Howard equivalent of Hilbert style proof systems inductively allowing judgements of the form |- s : A, where s is a proof term and A is a formula. In particular we will look at these combinators:
I:A->A /* (I x) = x */
K:A->(B->A) /* ((K x) y) = x */
W:(A->(A->B))->(A->B) /* ((W x) y) = ((x y) y) */
S:(A->(B->C))->((A->B)->(A->C)) /* (((S x) y) z) = ((x z) (y z)) */
B:(B->C)->((A->B)->(A->C)) /* (((B x) y) z) = ( x (y z)) */
C:(A->(B->C))->(B->(A->C)) /* (((C x) y) z) = ((x z) y ) */
In above we have put in comments the original definitions found in Moses Schönfinkels paper from 1918. What has changed since then are the mnemonics of the combinators, whereas the paper used I, C, T, Z, S we nowadays use I, K, C, B, S.
Type Inference
The Prolog realization of combinatory logics is based on providing a binary predicate typeof(s, A) that models the judgement |- s : A. In the below we have only one axiom schame I : A -> A, to avoid cyclic terms we need to use unify_with_occurs_check/2.
% Modus Ponens
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
% I Axiom
typeof(i, (A -> C)) :-
unify_with_occurs_check(A, C).
Etc..
By directly calling the predicate typeof/2 in mode (+, -) we can force a Prolog interpreter to perform a syntax directed reduction of the given combinatorial expression:
?- typeof(i*i, X).
X = (_39614 -> _39614).
By the nature of Prolog unification the result will be a most general type, whereby variables in the result can be replaced by arbitrary ground types still making a valid deduction.
Type Inhabitation
The type inhabitation problem asks a different question, we seek a proof term for a given formula. This cannot be directly solved via a Prolog interpreter, since a call of typeof/2 in mode (-, +) usually doesn't terminate, since modus ponens is left recursive. The root cause is Prologs depth first search strategy which is an incomplete method. Using meta programming we can replace the default search strategy by a form of iterative deepening:
search(true, N, N).
search((A,B), N, M) :-
search(A, N, H),
search(B, H, M).
search(typeof(P, T), N, M) :- N > 0, H is N-1,
clause(typeof(P, T), B),
search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
unify_with_occurs_check(A,B).
Since we count each typeof/3 invocation this means we count each modus ponens inference step and each axiom schema instantiation:
?- between(1,5,N), search(typeof(X, (a->a)), N, 0).
N = 1, X = i;
N = 3, X = i*i;
N = 5, X = i*i*i;
N = 5, X = i*(i*i);
fail.
Weakening and Contraction
A substructural logic is a logic that rejects some structural rules such as weakening or contraction. In a simple setting weakening and contraction can be identified with the types of the K combinator respectively the W combinator.
We consider Minimal Logic (SK), Affine Logic (BCK), Relevant Logic (SBCI)
and Linear Logic (BCI). We can already put some order into these logics by using our search predicate, in that we find type equalities:
I ~ ((S K) K) ~ ((C K) K)
B ~ (S (K S) K)
C ~ ((S (S (K (S (K S) K)) S) (K K))
W ~ ((S S) (S K)) ~ ((C S) I)
From the derivability of the types of the B combinator and C combinator in minimal logic, we can conclude that Affine ⊂ Minimal. Further the derivability of the type of I combinator allows us the conclusion Relevant ⊂ Minimal.
Further since the type of the I combinator is derivable in affine logic, we can further conclude Linear ⊂ Affine. Finally by definition it holds trivially Linear ⊂ Relevant. The two derivation for the W combinator gives us:
| Logic | Weakening (K) | Contraction (W) |
|---|---|---|
| Minimal (SK) | Yes | Yes |
| Affine (BCK) | Yes | |
| Relevant (SBCI) | Yes | |
| Linear (BCI) |
We left the negative results blank in the table, since we only tried a limited number of iterative deepening and did never establish an upper bound. In the next sections we will present more rigorous separation result.
McCunes Algorithm
William McCunes mace4 computer program is a counter model finder. We did a Prolog implementation that is not restricted to clauses and literals, rather supports arbitrary formulas. Likewise we also started supporting equality (=)/2 and universal quantifiers ![X], so that we could formulate problems from algebra:
problem(1, (
(![X]:(0*X = X) &
![X]:(X*0 = X) &
![X]:![Y]:![Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
It happens that this problem can be readily solved:
?- problem(1,F), solve(F, 3, R), !, show(R), fail.
a = 1 b = 2
0*0 = 0 0*1 = 1 0*2 = 2
1*0 = 1 1*1 = 1 1*2 = 1
2*0 = 2 2*1 = 2 2*2 = 2
fail.
Multi-Value Interpretation
To settle the question whether the inclusions Affine ⊂ Minimal, Relevant ⊂ Minimal, Linear ⊂ Affine and Linear ⊂ Relevant are proper or not, we will try to find multi-valued interpretations that separate the logics.
Instead of solving algebra problems we can use McCunes counter model finder to solve logic problems. The approach is to see logical connectives through the lense of algebra, considering (->)/2 a binary operation on truth values:
|- A -> B |- A
-------------------- (Modus Ponens)
|- B
-------- (Axiom Schema i)
|- A_i
We erase the combinatory expression s from the judgment |- s : A and consider judgment |- A. We do not ask for a congruence relation, only a consequence relation. We can now show that Affine Logic (BCK) does not generally admit contraction:
problem(2, (
(![X]:![Y]:t((X -> (Y -> X))) &
![X]:![Y]:(t((X -> Y)) & t(X) => t(Y)) &
![X]:![Y]:![Z]:t(((Y -> Z) -> ((X -> Y) -> (X -> Z)))) &
![X]:![Y]:![Z]:t(((X -> (Y -> Z)) -> (Y -> (X -> Z)))))
=> t(((a->(a->b))->(a->b))))).
The first found counter model is a three-valued logic, not from some text book:
?- between(1,3,N), problem(2, F), solve(F, N, R), !,
show(R), fail.
a = 1 b = 2
t(0) = 1 t(1) = 0 t(2) = 0
(0 -> 0) = 0 (0 -> 1) = 1 (0 -> 2) = 2
(1 -> 0) = 0 (1 -> 1) = 0 (1 -> 2) = 1
(2 -> 0) = 0 (2 -> 1) = 0 (2 -> 2) = 0
fail.
Separation Results
In summary it turns out that an according t/1 predicate for singled out truth values leads to relative short counter models that separate the investigated logics. We didn't need to go beyond three valued logics.
| Logic | Weakening (K) | Contraction (W) |
|---|---|---|
| Minimal (SK) | ||
| Affine (BCK) | No | |
| Relevant (SBCI) | No | |
| Linear (BCI) | No | No |
Each of the found counter model gives an invariant valuation. If the type in question then has an assignment outside of the invariant valuation, we know the type in question isn't generally valid and hence has no proof.
But it is not the case that an arbitrarly picked multi-valued interpretation gives automatically an invariant valuation, that would discriminate all unprovable formulas.
Conclusions
Links to Dogelog Notebooks that capture the proof finder and the model finder are given at the end of the post. We have practically automatized the work of a Logician in the middle of the previous century. We could determine proper inclusions relationships among the examined Minimal, Affine, Relevant and Linear logics.
Example 41: Hilbert-Style Calculus
https://www.xlog.ch/runtab/doclet/docs/06_demo/advent/example41/package.html
Example 42: Multi-Value Interpretation
https://www.xlog.ch/runtab/doclet/docs/06_demo/advent/example42/package.html