—————————————————————————————————————————————————————— | 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'