——————————————————————————————————————————————————————
| On the differences between Urban's calculi for LK, |
| Lengrand's λξ, van Bakel et al' X and Summers' X^i |
——————————————————————————————————————————————————————
Written May 2011, prepared for publication on April 2014
(I use hybrid notations from λξ alias X, the dual calculus and μμ~)
1) Urban's (T,cut)
- it has effective substitutions
- it is proved terminating
- it is apparently motivated by being the most faithful to the
standard approaches (?)
- it has the following key behavior of substitution on axioms:
[α=y.c] → c[x/y]
[x=β.c] → c[α/β]
2) Urban's (T,aux)
- has a more lambda-calculus-like substitution
- is adequate (according to Urban) for applying Barbanera-Berardi's
proof method
- it is rephrased (untyped) with name X^i in Alexander Summers' PhD
- it has the following key behavior of substitution on axioms:
[α=y.c] → .α † y.c
[x=β.c] → β.c † x.
(c.β † x.) [α=y.c'] → c.β[α=y.c'] † y.c'
(.α † y.c) [x=β.c'] → c'.β † y.c[x=β.c']
The last two steps are ad hoc but necessary to get normalisation
3) Urban's (T^↔,loc)
- like (T,aux) but with (two kinds) of explicit substitutions
represented by cuts (cut← and cut→)
- this is more faithful to the local cut-elimination procedures
- this is the same as λξ but not as X
- it has the following key behavior of substitution on axioms:
.α †← y.c → .α † y.c
c.β †→ x. → c.β † x.
(c.β † x.).α †← y.c' → (c.α †← y.c').β † y.c'
c'.β †→ x.(.α † y.c) → c'.β † y.(c'.β †→ x.c)
Again, the last two steps are ad hoc but necessary to get normalisation
3) X
- like (T^↔,loc) but without the ad hoc rule
- this gives a more uniform presentation but it looses termination
- indeed, it has the following key behavior of substitution on axioms:
.α †← y.c → .α † y.c
c.β †→ x. → c.β † x.
(c.β † x.).α †← y.c' → (c.α †← y.c').β † x.(.α †← y.c')
c'.β †→ x.(.α † y.c) → (c'.β †→ x.).α † y.(c'.β †→ x.c)
Remark 1: the non-terminating contraction/contraction pair (exemple
2.1.3 in Urban) comes from the use of the following reduction rules
(in μμ~ syntax):
<μ α.c(α,α) | e> → <μ α₁.< μ α₂.c(α₁,α₂) | e > | e>
→ >
Then, if for instance c(α,α) is and c(x,x) is <(x,x)|β>, then
<μα. | μ~x.<(x,x)|β>
→ <μα₁.(μα₂. | μ~x.<(x,x)|β>) | μ~x.<(x,x)|β>
→ <μα₁.(μα₂. | μ~x₁.<μα₂. | μ~x₂(x₁,x₂)|β>) | μ~x.<(x,x)|β>
and a new cut between contracted α₁ and contracted x occurs again.
Remark 2: the non-terminating reduction in X, taken from Summers, is
the following (we assume for simplicity that c do not contain α):
(c.β † x.) [α=y.c'] → c.β † (.x † y.c')
→ (.x † y.c') [x=β.c]
→ (c.β † x.).α † y.c'