1. Introduction
Confluence is one of the most important properties of rewriting systems. It means that the result of computation does not depend on the order of the computation. In general, it is hard to prove confluence for higher-order rewriting such as (extensions of) the lambda calculus. There is a long history of how to give simple and elegant proofs for confluence of lambda calculi: Church and Rosser’s proof with the notion of residuals of redexes, Tait and Martin-Löf’s proofs with parallel reduction, and Takahashi’s proof with complete developments. Hindley-Rosen’s method with commutation of several kinds of reductions is widely applicable for the lambda calculi extended by some reduction rules.
The Z theorem by Dehornoy and van Oostrom (Reference Dehornoy and van Oostrom2008), van Oostrom (Reference van Oostrom2021) is one of such elegant techniques, and it is widely applicable to confluence proofs in abstract settings. The Z theorem says that confluence of an abstract rewriting system follows from the existence of a mapping f satisfying the following Z property: any one-step reduction a → b implies b→*f(a)→*f(b), where →* is the reflexive transitive closure of →. It becomes clear why they call it the Z property when one draws the condition as the following diagram.
The mapping f that satisfies the Z property gives an abstract essence of developments without relying on the syntax of terms. If we define
$a \stackrel{f}{\to } b$
by a→*b→*f(a), then the Z property is equivalent to Takahashi’s angle property:
$a\stackrel{f}{\to }b$
implies
$b\stackrel{f}{\to }f(a)$
. The Z theorem has been applied to some variants of the lambda calculus in Accattoli and Kesner (Reference Accattoli and Kesner2012), Dehornoy and van Oostrom (Reference Dehornoy and van Oostrom2008), Reference Komori, Matsuda and YamakawaKomori et al. (2013), Nakazawa and Nagai (Reference Nakazawa and Nagai2014).
The Z property is not only a tool to prove confluence but it is also useful for quantitative analyses of the Church-Rosser property as Fujita (Reference Fujita2020) shows. The Z property is strictly stronger than confluence; that is, there are confluent rewrite systems for which no mapping satisfies the Z property. The following example is introduced by Dehornoy and van Oostrom (Reference Dehornoy and van Oostrom2008). Let A be the set of integers and n → m mean either (m = n + 1) or (n < 0 and m = − n), and then, the abstract rewriting system (A,→) is confluent but there is no mapping that satisfies the Z property. Hence, it is an interesting problem whether rewriting systems satisfy not only confluence but also the Z property.
Nakazawa and Fujita (Reference Nakazawa and Fujita2016) have proposed a variant of the Z theorem, called the compositional Z theorem. The compositional Z theorem enables us to apply the Z theorem by dividing rewriting systems into two or more subsystems. Compositional Z gives a simple proof of confluence of the lambda-mu calculus with permutation rules for direct sums. The original confluence proof by Ando (Reference Ando2003) for that system is more complex, and one cannot naively apply the original Z theorem because it is hard to directly define a mapping satisfying the Z property for both beta and permutation reductions. Moreover, Reference Honda, Nakazawa and FujitaHonda et al. (2021) adapted the compositional Z theorem to several variants of the lambda-mu calculus with simplification rules.
Carraro and Guerrieri (Reference Carraro and Guerrieri2014) introduced λ
v
σ
, a call-by-value variant of the lambda calculus with strong reduction (reductions under lambda abstractions are allowed) for open terms. If we naively consider call-by-value computations for open terms, there exist terms that are neither a normal form nor a value such as xx, and then, the term (λy.λz.zz)(xx)(λz.zz) cannot be reduced while it morally contains the redex (λz.zz)(λz.zz), which diverges. To avoid such unexpected stucks of computation, they adopted some permutation rules. In Accattoli and Guerrieri (Reference Accattoli and Guerrieri2016), this calculus is also called the shuffling calculus
$\lambda _{\sf shuf}$
and further discussed as one of the call-by-value variants of the lambda calculus for open terms. As with the permutation rules for the direct sums, the permutation rules of λ
v
σ
make the proof of confluence harder, and one cannot straightforwardly adapt the ordinary proof techniques resting on parallel reduction or complete developments. Carraro and Guerrieri proved confluence of λ
v
σ
using Hindley-Rosen’s method, in which they proved that β
v
reduction and the permutation rules commute and that the permutation rules are strongly normalizing.
In this paper, we give another proof of confluence for the shuffling calculus λ v σ using the compositional Z theorem. This proof provides a case study of applications of the (compositional) Z theorem to extensions of the lambda calculi with some additional reduction rules. Our proof does not depend on any normalization property of the reduction relation, and it differs from the existing proof by Carraro and Guerrieri (Reference Carraro and Guerrieri2014), where the strong normalization of the permutation reduction is used. As with Nakazawa and Fujita (Reference Nakazawa and Fujita2016), we cannot naively apply the original Z theorem for λ v σ , and the problem can be avoided by the compositional Z. Although the outline of our proof follows the proof of Nakazawa and Fujita (Reference Nakazawa and Fujita2016), the main difference is that the mapping we consider here may leave redexes of permutation reductions since the calculus has two kinds of permutation rules σ 1 and σ 3 for the call-by-value evaluation context []M and V[], respectively, for a term M and a value V. Hence, we cannot apply the simplified variant of the compositional Z (Corollary 2.4 in Nakazawa and Fujita Reference Nakazawa and Fujita2016).
This paper is the extended version of the conference proceeding, Reference Nakazawa, Fujita and ImagawaNakazawa et al. (2017).
2. The Shuffling Calculus λ v σ
In this section, we recall the call-by-value lambda calculus λ v σ introduced by Carraro and Guerrieri (Reference Carraro and Guerrieri2014).
We use the following notation throughout this paper: syntactic equality is denoted by =. For a binary relation R, we use R + and R* for the transitive closure of R and the reflexive transitive closure of R, respectively.
Definition 1. Values and terms of λ v σ are given as follows.
\begin{align*} V & ::= x \mid \lambda x.M & \mbox{(values)}\\ M & ::= V \mid M M & \mbox{(terms)} \end{align*}
We define the size of M as the number of occurrences of the symbols in M. We define the free variables of M as usual, and the set of the free variables of M is denoted by FV(M). A relation R on the terms is compatible if M R M′ implies (λx.M) R (λx.M′), (MN) R (M′N), and (NM) R (NM′).
The reduction rules of λ v σ are given as follows.
\begin{align*} (\lambda x.M)V & \to _{\beta _v} M{[{x}:={V}]} \\ (\lambda x.M)NL & \to _{\sigma _1} (\lambda x.ML)N & \mbox{($x\not \in FV(L)$)}\\ V((\lambda x.M)N) & \to _{\sigma _3} (\lambda x.VM)N & \mbox{($x\not \in FV(V)$)} \end{align*}
Here, V is a value, M, N, and L are terms, and M[x:=V] is the usual capture-avoiding substitution. The relations → β v , → σ 1 , and → σ 3 are the compatible closure of the reduction relation defined by the corresponding reduction rules, respectively. We define → σ as the union of → σ 1 and → σ 3 . We define → as the union of → β v and → σ .
This calculus is introduced in Carraro and Guerrieri (Reference Carraro and Guerrieri2014) to study operational characterization of solvability in call-by-value lambda calculi in particular for open terms. In the original call-by-value lambda calculus λ v of Plotkin (Reference Plotkin1975), the term M = (λyx.xx)(zz)(λx.xx) is stuck since zz is not a value, whereas semantically it is equivalent to (λx.xx)(λx.xx) and hence unsolvable. In λ v σ , M is reduced to (λy.(λx.xx)(λx.xx))(zz) by the σ-rules, where the redex (λx.xx)(λx.xx) is no longer blocked.
3. Compositional Z
We summarize the Z theorem of Dehornoy and van Oostrom (Reference Dehornoy and van Oostrom2008) and then extend it for compositional functions, called the compositional Z of Nakazawa and Fujita (Reference Nakazawa and Fujita2016).
Definition 2. ((Weak) Z property)
Let (A, → ) be an abstract rewriting system and
$\,{\to _{{\sf x}}}\,$
be another relation on A.
1. A mapping f satisfies the weak Z property for → by
$\,{\to _{{\sf x}}}\,$
if and only if a → b implies
$b{\,{\to ^*_{{\sf x}}}\,} f(a){\,{\to ^*_{{\sf x}}}\,} f(b)$
for any a, b ∈ A.
2. A mapping f satisfies the Z property for → if and only if it satisfies the weak Z property for → by → .
When f satisfies the (weak) Z property, we also say that f is (weakly) Z.
Theorem 3. (Z theorem by Dehornoy and van Oostrom (2008)) If there exists a mapping satisfying the Z property for an abstract rewriting system, then it is confluent.
We can often prove that usual complete developments have the Z property.
Theorem 4. (Compositional Z by Nakazawa and Fujita Reference Nakazawa and Fujita2016) Let (A, → ) be an abstract rewriting system, and → be →1 ∪ →2 . If there exist mappings f 1, f 2 : A → A such that
-
1. f 1 is Z for →1
-
2. a →1 b implies f 2(a) →* f 2(b)
-
3. a →* f 2(a) holds for any a ∈ Im(f 1)
-
4. f 2 ∘ f 1 is weakly Z for →2 by → ,
then f 2 ∘ f 1 is Z for (A, → ), and hence (A, → ) is confluent.
One of the simplest applications of the compositional Z is for the βη-reduction on the untyped lambda calculus (although it can be directly proved by the original Z theorem, as Reference Komori, Matsuda and YamakawaKomori et al. (2013) showed). If we let →1 be → η , →2 be → β , f 1 be the complete development of → η , and f 2 be the complete development of → β , then these satisfy the conditions of the compositional Z theorem.
In Nakazawa and Fujita (Reference Nakazawa and Fujita2016), the compositional Z is applied to the lambda calculus with permutation rules for direct sums. This calculus is a lambda calculus extended with two inclusion operators ι
1
M, ι
2
M into direct sums and the case expression
$({\sf case}\ M\ {\sf with}\ \iota _1 x_1\Rightarrow N_1 \mid \ \iota _2 x_2\Rightarrow N_2)$
. For simplicity, this case expression is denoted as M[x
1.N
1,x
2.N
2] in Nakazawa and Fujita (Reference Nakazawa and Fujita2016). The additional reduction rules are
\begin{align*} (\iota _1 M)[x_1.N_1,x_2.N_2] & \to _\beta N_1[x_1:=M],\\ (\iota _2 M)[x_1.N_1,x_2.N_2] & \to _\beta N_2[x_2:=M],\\ E[M[x_1.N_1,x_2.N_2]] & \to _\pi M[x_1.E[N_1],x_2.E[N_2]], \end{align*}
where E denotes singular destructor contexts defined as E : := []L ∣ [][y 1.K 1,y 2.K 2] ∣ . The last rule is called the permutation rule, and it makes confluence proofs much harder because of the following critical pair: for the term P[x 1.N 1,x 2.N 2][y 1.L 1,y 2.L 2]K, we have
\begin{align*} \underline{P[x_1.N_1,x_2.N_2][y_1.L_1,y_2.L_2]}K & \to _\pi P[x_1.N_1 [y_1.L_1,y_2.L_2],x_2.N_2[y_1.L_1,y_2.L_2]]K (\!{=}\! M_1) \\ \mbox{and } \underline{P[x_1.N_1,x_2.N_2][y_1.L_1,y_2.L_2]K} & \to _\pi P[x_1.N_1,x_2.N_2][y_1.L_1 K,y_2.L_2 K] (\!{=}\! M_2), \end{align*}
where the underlines indicate the redexes of the permutation reductions. Both M 1 and M 2 can be reduced to a common term M 3 = P[x 1.N 1[y 1.L 1 K,y 2.L 2 K],x 2.N 2[y 1.L 1 K,y 2.L 2 K]], but in M 1→*M 3 we have to reduce a redex which is created during the reduction sequence and does not occur in M 1. Because of this, it is hard to apply straightforwardly either the ordinary parallel reduction or the original Z theorem. In Nakazawa and Fujita (Reference Nakazawa and Fujita2016), the compositional Z theorem is applied to this calculus by dividing the reduction relations into two parts, the β-reduction and the permutations, and defining two mappings, one for the β-reduction and the other for the permutations, satisfying the assumptions of the compositional Z theorem.
4. Confluence of λ v σ by the Compositional Z
In this section, we see that λ v σ contains similar critical pairs to those in the lambda calculus with direct sums and that the compositional Z solves the problem.
4.1 Difficulties in confluence proof for λ v σ
Consider the term (λx.N)((λy.K)L)P. Then, we have both
\begin{align*} \underline{(\lambda x.N)((\lambda y.K)L)P} & \to _{\sigma _1}{=} (\lambda x.NP)((\lambda y.K)L)(\!{=}\! M_1)\\ \mbox{and } \underline{(\lambda x.N)((\lambda y.K)L)}P & \to _{\sigma _3} (\lambda y.(\lambda x.N)K)LP(\!{=}\! M_2), \end{align*}
where the underlines indicate the redexes. The terms M 1 and M 2 are reduced to a common term M 3 = (λy.(λx.NP)K)L. M 1 → M 3 is one-step σ 3 reduction, whereas M 2→*M 3 consists of two σ 1 steps:
$$ M_2 {=} \underline {(\lambda y.(\lambda x.N)K)LP} \to _{\sigma _1} \underline {(\lambda y.(\lambda x.N)KP)}L \to _{\sigma _1} (\lambda y.(\lambda x.NP)K)L, $$
where the redex of the second σ 1-step is created at the first step and it does not occur in M 2. This means that we cannot naively extend the ordinary parallel reduction, by which M 2 is not reduced to M 3 in one step. To define a mapping satisfying the Z property, we have to reduce successive σ-reductions at once. For example, the above example shows that M must be mapped to M 3 or some of its reducts.
In Nakazawa and Fujita (Reference Nakazawa and Fujita2016), they considered the auxiliary mapping M@N such as
$$ (\lambda y.(\lambda x.N)K)L@P {=} (\lambda y.(\lambda x.N@P)K)L, $$
which yields the normal form for the permutation reduction. Here, there are two kinds of permutation rules σ 1 and σ 3 and we consider the following two auxiliary mappings.
Definition 5. We define the mappings @1 and @3 as follows.
\begin{align*} (\lambda x.M)N @_1 P & {=} (\lambda x.M @_1 P)N & V @_3 (\lambda x.M)N & {=} (\lambda x.V @_3 M)N\\ M @_1 P & {=} MP \quad \mbox{(otherwise)} & V @_3 M & {=} VM \quad \mbox{(otherwise)} \end{align*}
However, similarly to the case of the direct sums, the following naive mapping does not satisfy the Z property.
\begin{align*} x^* & {=} x\\ (\lambda x.M)^* & {=} \lambda x.M^*\\ ((\lambda x.M)V)^* & {=} M^*{[{x}:={{V^*}}]} \\ (MN)^* & {=} M^* @_1 N^* \quad \mbox{($M$ not a value)} \\ (VN)^* & {=} V^* @_3 N^* \quad \mbox{(otherwise)} \end{align*}
For P = (λx.xy)(λz.z)v and Q = (λx.xyv)(λz.z), we have P→ σ 1 Q, but we also have P* = (λz.z)y@1 v = (λz.zv)y and Q* = (λz.z)yv, and hence, P*↛*Q*. In Q*, the substitution (xyv)[x:=λz.z] creates the σ 1-redex (λz.z)yv, and it is not reduced.
4.2 Confluence proof of λ v σ by applying the compositional Z theorem
We solve this problem by the compositional Z theorem. To apply it, we divide the reductions of λ
v
σ
into σ and β
v
, and define the mappings
$(\!\cdot \!)^{\sf S}$
and
$(\!\cdot \!)^{\sf B}$
.
Definition 6.
We define the mappings
$(\!\cdot \!)^{\sf S}$
and
$(\!\cdot \!)^{\sf B}$
as follows.
\begin{align*} x^{\sf S} & {=} x & x^{\sf B} & {=} x \\ (\lambda x.M)^{\sf S} & {=} \lambda x.M^{\sf S} & (\lambda x.M)^{\sf B} & {=} \lambda x.M^{\sf B}\\ (MN)^{\sf S} & {=} M^{\sf S} @_1 N^{\sf S} \quad \mbox{($M$ not a value)} & ((\lambda x.M)V)^{\sf B} & {=} M^{\sf B}{[{x}:={{V^{\sf B}}}]}\\ (VN)^{\sf S} & {=} V^{\sf S} @_3 N^{\sf S} & (MN)^{\sf B} & {=} M^{\sf B}N^{\sf B} \quad \mbox{(otherwise)} \end{align*}
In the following, we show that these mappings satisfy the conditions of the compositional Z theorem.
The outline of the proof almost follows the proof in Nakazawa and Fujita (Reference Nakazawa and Fujita2016). However, in contrast to that proof, the mapping
$(\!\cdot \!)^{\sf S}$
does not necessarily collapse all σ-steps; that is, there are terms M and N such that M→
σ
N and
$M^{\sf S}\to ^+_\sigma N^{\sf S}$
. For example, we have
$$ M {=} (\lambda x.x)(yz)((\lambda v.v)w) \to _{\sigma _1} (\lambda x.x((\lambda v.v)w))(yz) {=} N, $$
and
\begin{align*} M^{\sf S} & {=} ((\lambda x.x)(yz))^{\sf S}@_1((\lambda v.v)w)^{\sf S}{=} (\lambda x.x((\lambda v.v)w))(yz)\\ N^{\sf S} & {=} (\lambda x.x((\lambda v.v)w))^{\sf S}@_3(yz)^{\sf S}{=} (\lambda x.x @_3 ((\lambda v.v)w))(yz){=} (\lambda x.(\lambda v.xv)w)(yz), \end{align*}
The σ
3-redex x((λv.v)w) in
$M^{\sf S}$
is created in the application of
$(\!\cdot \!)^{\sf S}$
, and it is not reduced in
$M^{\sf S}$
. Hence, we cannot apply the simplified variant of compositional Z (Corollary 2.4 in Nakazawa and Fujita Reference Nakazawa and Fujita2016) for these mappings.
From here, we prove the conditions of Theorem 4, where we consider →
σ
as →1, →
β
v
as →2,
$(\!\cdot \!)^{\sf S}$
as f
1, and
$(\!\cdot \!)^{\sf B}$
as f
2.
First, we prove auxiliary lemmas concerning the properties of the mappings @1, @3, and
$(\!\cdot \!)^{\sf S}$
.
Lemma 7. For any value V and any terms M, N, we have the following.
-
1.
$VM\to ^*_\sigma V @_3 M$
. -
2.
$MN\to ^*_\sigma M @_1 N$
.
Proof. They are proved by induction on the size of M.
-
1. If M = (λx.L)K, we have
Otherwise, we have VM = V@3 M.
\begin{align*} V((\lambda x.L)K) & \to _{\sigma _3} (\lambda x.VL)K \\ & \to ^*_{\sigma } (\lambda x.V @_3 L)K & \mbox{(induction hypothesis)}\\ & = V @_3(\lambda x.L)K. \end{align*}
-
2. It is proved similarly.
Lemma 8. For any terms M and N, we have the following.
-
1.
$M^{\sf S}@_1 N^{\sf S} \to ^*_\sigma (MN)^{\sf S}$
. -
2.
$M^{\sf S}N^{\sf S} \to ^*_\sigma (MN)^{\sf S}$
.
Proof.
-
1. If M is not a value, we have
$M^{\sf S}@_1 N^{\sf S} = (MN)^{\sf S}$
. If M is a value, we have
$M^{\sf S}@_1 N^{\sf S}= M^{\sf S} N^{\sf S} \to ^*_\sigma M^{\sf S}@_3 N^{\sf S} = (MN)^{\sf S}$
by Lemma 7. -
2. By Lemma 7 and (1), we have
$M^{\sf S}N^{\sf S} \to ^*_\sigma M^{\sf S} @_1 N^{\sf S} \to ^*_\sigma (MN)^{\sf S}$
.
Lemma 9. For any value V and any terms M, N, K, we have the following.
-
1. ((λx.M)@3 N)@1 K = (λx.M@1 K)@3 N.
-
2. V@3((λx.M)@3 N) = (λx.V@3 M)@3 N.
Proof. They are proved by induction on the size of N.
-
1. If N = (λy.P)Q, we have
Otherwise, by the definitions of @1 and @3, we have ((λx.M)@3 N)@1 K = ((λx.M)N)@1 K = (λx.M@1 K)N = (λx.M@1 K)@3 N.
\begin{align*} ((\lambda x.M)@_3 ((\lambda y.P)Q))@_1 K & = (\lambda y.((\lambda x.M)@_3 P)@_1 K)Q & \mbox{(def. of $@_1$ and $@_3$)}\\ & = (\lambda y.(\lambda x.M @_1 K)@_3 P)Q & \mbox{(induction hypothesis)}\\ & = (\lambda x.M @_1 K)@_3((\lambda y.P)Q) & \mbox{(def. of $@_3$).} \end{align*}
-
2. It is proved similarly.
We prove the following lemma. The second property means that the condition (3) of Theorem 4 holds.
Lemma 10. For any term M, we have the following.
-
1.
$M\to ^*_\sigma M^{\sf S}$
. -
2.
$M\to ^*_{\beta _v} M^{\sf B}$
.
Proof. They are proved by induction on the size of M.
-
1. In the case of M = NK, we have
$NK\to ^*_\sigma N^{\sf S}K^{\sf S}$
by the induction hypothesis, and
$N^{\sf S}K^{\sf S} \to ^*_\sigma (NK)^{\sf S}$
by Lemma 8. In the case of M = x, it is trivial. In the case of M = λx.N, it is proved by the induction hypothesis. -
2. In the case of M = NK, we consider the following cases. If N = λx.L and K is a value, we have
Otherwise, we have
\begin{align*} (\lambda x.L)V & \to _{\beta _v} L{[{x}:={V}]}\\ & \to ^*_{\beta _v} L^{\sf B}{[{x}:={{V^{\sf B}}}]} & \mbox{(induction hypothesis)}\\ & =((\lambda x.L)V)^{\sf B}. \end{align*}
$(NK)^{\sf B}=N^{\sf B}K^{\sf B}$
, and
$NK\to ^*_{\beta _v}N^{\sf B}K^{\sf B}$
holds by the induction hypothesis. In the case of M = x, it is trivial. In the case of M = λx.N, it is proved by the induction hypothesis.
The next goal is to prove that the condition (1) of Theorem 4 holds; that is,
$(\!\cdot \!)^{\sf S}$
is Z for →
σ
(Propositions 12 and 15).
The following lemma is used to prove the cofinality (Proposition 12): M→
σ
M′ implies
$M'\to ^*_\sigma M^{\sf S}$
.
Lemma 11. For any value V and any terms M, N, K, we have the following.
-
1. If x ∉ FV(K), we have
$(\lambda x.MK)N \to ^*_\sigma ((\lambda x.M)@_3 N)@_1 K$
. -
2. If x ∉ FV(V), we have
$(\lambda x.VM)N \to ^*_\sigma V @_3 ((\lambda x.M)@_3 N)$
.
Proof. They are proved by induction on the size of N.
-
1. If N = (λy.P)Q, we have
Otherwise, we have
\begin{align*} (\lambda x.MK)((\lambda y.P)Q) & \to _{\sigma _3} (\lambda y.(\lambda x.MK)P)Q\\ & \to ^*_\sigma (\lambda y.((\lambda x.M)@_3 P)@_1 K)Q & \mbox{(induction hypothesis)}\\ & = ((\lambda y.(\lambda x.M)@_3 P)Q)@_1 K & \mbox{(definition of $@_1$)}\\ & = ((\lambda x.M)@_3(\lambda y.P)Q)@_1 K & \mbox{(definition of $@_3$).} \end{align*}
\begin{align*} (\lambda x.MK)N & \to ^*_\sigma (\lambda x.M @_1 K)N & \mbox{(Lemma 7 (2))}\\ & =((\lambda x.M)N)@_1 K & \mbox{(definition of $@_1$)}\\ & = ((\lambda x.M)@_3 N)@_1 K & \mbox{(definition of $@_3$).} \end{align*}
-
2. If N = (λy.P)Q, we have
Otherwise, we have
\begin{align*} (\lambda x.VM)((\lambda y.P)Q) & \to _{\sigma _3} (\lambda y.(\lambda x.VM)P)Q\\ & \to ^*_\sigma (\lambda y.V @_3 ((\lambda x.M)@_3 P)Q & \mbox{(induction hypothesis)}\\ & = V @_3 (\lambda y.((\lambda x.M)@_3 P)Q & \mbox{(definition of $@_3$)}\\ & = V @_3 ((\lambda x.M) @_3 (\lambda y.P)Q) & \mbox{(definition of $@_3$).} \end{align*}
\begin{align*} (\lambda x.VM)N & \to ^*_\sigma (\lambda x.V @_3 M)N & \mbox{(Lemma 7 (1))}\\ & = V @_3((\lambda x.M)N) & \mbox{(definition of $@_3$)}\\ & = V @_3((\lambda x.M) @_3 N) & \mbox{(definition of $@_3$).} \end{align*}
Proposition 12.
For any terms M and M′, if M→
σ
M′ holds, then
$M'\to ^*_\sigma M^{\sf S}$
holds.
Proof. By induction on a derivation of M→ σ M′.
First, the base cases are proved as follows.
If M = (λx.P)QK and M′ = (λx.PK)Q, we have
\begin{align*} (\lambda x.PK)Q & \to ^*_\sigma (\lambda x.P^{\sf S}K^{\sf S})Q^{\sf S} & \mbox{(Lemma 10)}\\ & \to ^*_\sigma ((\lambda x.P^{\sf S})@_3 Q^{\sf S})@_1 K^{\sf S} & \mbox{(Lemma 11)}\\ & =((\lambda x.P)QK)^{\sf S} & \mbox{(definition of S).} \end{align*}
If M = V((λx.P)Q) and M′ = (λx.VP)Q, it is proved similarly by Lemmas 10 and 11.
Next, we show the induction cases.
If M = λx.N, M′ = λx.N′, and N→
σ
N′, then, by the induction hypothesis, we have
$N'\to ^*_\sigma N^{\sf S}$
. Then, we have
$\lambda x.N' \to ^*_\sigma \lambda x.N^{\sf S}=(\lambda x.N)^{\sf S}$
.
If M = PQ, M′ = P′Q′, and either P→
σ
P′ and Q = Q′ or Q→
σ
Q′ and P = P′, then, by the induction hypothesis and Lemma 10, we have
$P'\to ^*_\sigma P^{\sf S}$
and
$Q'\to ^*_\sigma Q^{\sf S}$
. Then, we have
$P'Q'\to ^*_\sigma P^{\sf S}Q^{\sf S}\to ^*_\sigma (PQ)^{\sf S}$
by Lemma 8.
Therefore, we prove some lemmas to prove the monotonicity (Proposition 15): M→
σ
M′ implies
$M^{\sf S}\to ^*_\sigma{M'}^{\sf S}$
.
Lemma 13. For any values V, W and any terms M, N, we have the following.
-
1.
$(M@_1 N){[{x}:={V}]}\to ^*_\sigma M{[{x}:={V}]}@_1 N{[{x}:={V}]}$
. -
2.
$(W@_3 M){[{x}:={V}]}\to ^*_\sigma W{[{x}:={V}]}@_3 M{[{x}:={V}]}$
.
Proof. They are proved by induction on the size of M.
-
1. If M = (λy.P)Q, we have
Otherwise, we have
\begin{align*} (((\lambda y.P)Q)@_1 N){[{x}:={V}]} & = ((\lambda y.P@_1 N)Q){[{x}:={V}]} & \!\!\!\mbox{(definition of $@_1$)}\\ & = (\lambda y.(P@_1 N){[{x}:={V}]})Q{[{x}:={V}]}\\ & \to ^*_\sigma (\lambda y.P{[{x}:={V}]}@_1 N{[{x}:={V}]})Q{[{x}:={V}]} & \!\!\!\mbox{(induction hypothesis)}\\ & = ((\lambda y.P{[{x}:={V}]})Q{[{x}:={V}]})@_1 N{[{x}:={V}]} & \!\!\!\mbox{(definition of $@_1$)}\\ & = ((\lambda y.P)Q){[{x}:={V}]}@_1 N{[{x}:={V}]}. \end{align*}
$(M@_1 N){[{x}:={V}]} = M{[{x}:={V}]}N{[{x}:={V}]} \to ^*_\sigma M{[{x}:={V}]}@_1 N{[{x}:={V}]}$
by Lemma 7.
-
2. It is proved similarly.
We prove that the mappings @1 and @3 preserve the reductions → σ and → β v in the following sense. This is the main lemma for the monotonicity and is also used to prove that the conditions (2) and (4) of Theorem 4 hold.
Lemma 14. For any values V, V′ and any terms M, M′, N, N′, we have the following.
-
1. If M→ σ M′, then
$M@_1 N\to ^*_\sigma M'@_1 N$
and
$V @_3 M \to ^*_\sigma V @_3 M'$
hold.
-
2. If M→ β v M′, then M@1 N→*M′@1 N and V@3 M→*V@3 M′ hold.
-
3. For ξ ∈ {β v , σ}, if N→ ξ N′, then M@1 N→ ξ M@1 N′ holds.
-
4. For ξ ∈ {β v , σ}, if V→ ξ V′, then V@3 M→ ξ V′@3 M holds.
Proof. They are proved by induction on the size of M.
-
1. If M = (λx.P)Q, it is not a σ-redex, so M′ is (λx.P′)Q′ for some P′ and Q′ such that either P→ σ P′ and Q = Q′ or Q→ σ Q′ and P = P′. Then, we have
\begin{align*} ((\lambda x.P)Q) @_1 N & = ((\lambda x.P@_1 N)Q) & \mbox{(definition of $@_1$)}\\ & \to ^*_\sigma ((\lambda x.P'@_1 N)Q') & \mbox{(inductive hypothesis)}\\ & = ((\lambda x.P')Q')@_1 N & \mbox{(definition of $@_1$).} \end{align*}
Otherwise, we have
$M@_1 N = MN \to _\sigma M'N \to ^*_\sigma M'@_1 N$
by Lemma 7.The case @3 is proved similarly.
-
2. If M = (λx.P)V and M′ = P[x:=V], we have
If M = (λx.P)Q, M′ = (λx.P′)Q′, and either P→ β v P′ and Q = Q′ or Q→ β v Q′ and P = P′, we have
\begin{align*} ((\lambda x.P)V) @_1 N & = ((\lambda x.P@_1 N)V) & \mbox{(definition of $@_1$)}\\ & \to _{\beta _v} (P@_1 N){[{x}:={V}]}\\ & \to ^*_\sigma P{[{x}:={V}]}@_1 N & \mbox{(Lemma 13 and $x\not \in FV(N)$).} \end{align*}
\begin{align*} ((\lambda x.P)Q) @_1 N & = ((\lambda x.P@_1 N)Q) & \mbox{(definition of $@_1$)}\\ & \to ^* ((\lambda x.P'@_1 N)Q') & \mbox{(induction hypothesis)}\\ & = ((\lambda x.P')Q') @_1 N & \mbox{(definition of $@_1$).} \end{align*}
Otherwise, we have
$M@_1 N = MN \to _{\beta _v}M'N \to ^*_\sigma M'@_1 N$
by Lemma 7.The case @3 is proved similarly.
-
3. If M = (λx.P)Q, we have
Otherwise, we have M@1 N = MN→ ξ MN′ = M@1 N′.
\begin{align*} ((\lambda x.P)Q)@_1 N & = (\lambda x.P@_1 N)Q & \mbox{(definition of $@_1$)}\\ & \to _\xi (\lambda x.P@_1 N')Q & \mbox{(inductive hypothesis)}\\ & = ((\lambda x.P)Q)@_1 N' & \mbox{(definition of $@_1$).} \end{align*}
-
4. It is proved similarly.
Proposition 15.
For any terms M and M′, if M→
σ
M′ holds, then
$M^{\sf S}\to ^*_\sigma{M'}^{\sf S}$
holds.
Proof. By induction on a derivation of M→ σ M′.
First, the base cases are proved as follows.
If M = (λx.P)QK and M′ = (λx.PK)Q, we have
\begin{align*} ((\lambda x.P)QK)^{\sf S} & = ((\lambda x.P^{\sf S})@_3 Q^{\sf S}) @_1 K^{\sf S}\\ & = (\lambda x.P^{\sf S} @_1 K^{\sf S})@_3 Q^{\sf S} & \mbox{(Lemma 9 (1))}\\ & \to ^*_\sigma (\lambda x.(PK)^{\sf S})@_3 Q^{\sf S} & \mbox{(Lemmas 8 (1) and 14 (4))}\\ & = ((\lambda x.PK)Q)^{\sf S}. \end{align*}
If M = V((λx.P)Q) and M′ = (λx.VP)Q, we have
\begin{align*} (V((\lambda x.P)Q))^{\sf S} & = V^{\sf S} @_3 ((\lambda x.P^{\sf S}) @_3 Q^{\sf S})\\ & = (\lambda x.V^{\sf S} @_3 P^{\sf S}) @_3 Q^{\sf S} & \mbox{(Lemma 9 (2))}\\ & = ((\lambda x.VP)Q)^{\sf S}. \end{align*}
Next, the induction cases are proved as follows.
If M = λx.N, M′ = λx.N′, and N→
σ
N′, by the induction hypothesis, we have
$N^{\sf S}\to ^*_\sigma{N'}^{\sf S}$
. Then, we have
$(\lambda x.N)^{\sf S} = \lambda x.N^{\sf S} \to ^*_\sigma \lambda{x.N'}^{\sf S}=(\lambda x.N')^{\sf S}$
.
If M = PQ, M′ = P′Q′, and either P→
σ
P′, Q = Q′ or Q→
σ
Q′, P = P′, by the induction hypothesis, we have
$P^{\sf S}\to ^*_\sigma{P'}^{\sf S}$
and
$Q^{\sf S}\to ^*_\sigma{Q'}^{\sf S}$
. If P is not a value, we have
\begin{align*} (PQ)^{\sf S} & = P^{\sf S}@_1 Q^{\sf S}\\ & \to ^*_\sigma{P'}^{\sf S}@_1{Q'}^{\sf S} & \mbox{(Lemma 14 (1) and (3))}\\ & \to ^*_\sigma (P'Q')^{\sf S} & \mbox{(Lemma 8).} \end{align*}
If P is a value, we have
\begin{align*} (PQ)^{\sf S} & = P^{\sf S}@_3 Q^{\sf S}\\ & \to ^*_\sigma{P'}^{\sf S}@_3{Q'}^{\sf S} & \mbox{(Lemma 14 (1) and (4))}\\ & = (P'Q')^{\sf S} & \mbox{($P'$ is a value).} \end{align*}
We prove the condition (2) of Theorem 4 (Proposition 18).
Lemma 16. For any value V and any term M, we have the following.
-
1.
$M^{\sf S}{[{x}:={{V^{\sf S}}}]} \to ^*_\sigma M{[{x}:={V}]}^{\sf S}$
. -
2.
$M^{\sf B}{[{x}:={{V^{\sf B}}}]} \to ^*_{\beta _v} M{[{x}:={V}]}^{\sf B}$
.
Proof.
-
1. By induction on the size of M. If M = PQ and P is not a value, we have
If P is a value, it is proved similarly. The other cases are straightforward.
\begin{align*} (PQ)^{\sf S}{[{x}:={{V^{\sf S}}}]} & =(P^{\sf S}@_1 Q^{\sf S}){[{x}:={{V^{\sf S}}}]}\\ & \to ^*_\sigma P^{\sf S}{[{x}:={{V^{\sf S}}}]}@_1 Q^{\sf S}{[{x}:={{V^{\sf S}}}]} & \mbox{(Lemma 13)}\\ & \to ^*_\sigma P{[{x}:={V}]}^{\sf S}@_1 Q{[{x}:={V}]}^{\sf S} & \mbox{(induction hypothesis and Lemma 14 (1), (3))}\\ & = (P{[{x}:={V}]}Q{[{x}:={V}]})^{\sf S} & \mbox{(Lemma 8 (1))}\\ & = (PQ){[{x}:={V}]}^{\sf S}. \end{align*}
-
2. By induction on the size of M. If M = (λy.P)W, we have
If M = xW and V = λy.P, we have
\begin{align*} ((\lambda y.P)W)^{\sf B}{[{x}:={{V^{\sf B}}}]} & = P^{\sf B}{[{y}:={{W^{\sf B}}}]}{[{x}:={{V^{\sf B}}}]} & \mbox{(definition of B)}\\ & = P^{\sf B}{[{x}:={{V^{\sf B}}}]}{[{y}:={{W^{\sf B}{[{x}:={{V^{\sf B}}}]}}}]}\\ & \to ^*_{\beta _v} P{[{x}:={V}]}^{\sf B}{[{y}:={{W{[{x}:={V}]}^{\sf B}}}]} & \mbox{(induction hypothesis)}\\ & = ((\lambda y.P{[{x}:={V}]})W{[{x}:={V}]})^{\sf B} & \mbox{(definition of B)}\\ & = ((\lambda y.P)W){[{x}:={V}]}^{\sf B}. \end{align*}
\begin{align*} (xW)^{\sf B}{[{x}:={{(\lambda y.P)^{\sf B}}}]} & = (\lambda y.P^{\sf B})W^{\sf B}{[{x}:={{\lambda y.P^{\sf B}}}]}\\ & \to _{\beta _v} P^{\sf B}{[{y}:={{W^{\sf B}{[{x}:={{\lambda y.P^{\sf B}}}]}}}]}\\ & \to ^*_{\beta _v} P^{\sf B}{[{y}:={{W{[{{x}}:={{\lambda y.P}}]}^{\sf B}}}]} & \mbox{(induction hypothesis)}\\ & =((\lambda y.P)W{[{x}:={{\lambda y.P}}]})^{\sf B}\\ & =(xW){[{x}:={{\lambda y.P}}]}^{\sf B}. \end{align*}
The other cases are straightforward.
Lemma 17.
For any terms M and N, we have
$M^{\sf B}N^{\sf B}\to ^*_{\beta _v} (MN)^{\sf B}$
.
Proof.
If M is a value, we have
$M^{\sf B}N^{\sf B}= (xN)^{\sf B}{[{x}:={{M^{\sf B}}}]} \to ^*_{\beta _v} (xN){[{x}:={M}]}^{\sf B} = (MN)^{\sf B}$
by Lemma 16. If M is not a value, we have
$M^{\sf B}N^{\sf B}=(MN)^{\sf B}$
.
Proposition 18.
For any terms M and M′, if M→
σ
M′ holds, then
$M^{\sf B}\to ^*{M'}^{\sf B}$
holds.
Proof. By induction on a derivation of M→ σ M′.
First, the base cases are proved as follows.
If M = (λx.P)VK and M′ = (λx.PK)V, we have
\begin{align*} ((\lambda x.P)VK)^{\sf B} & = P^{\sf B}{[{x}:={{V^{\sf B}}}]}K^{\sf B} & \mbox{(definition of B)}\\ & = (P^{\sf B}K^{\sf B}){[{x}:={{V^{\sf B}}}]}\\ & \to ^*_{\beta _v}(PK)^{\sf B}{[{x}:={{V^{\sf B}}}]} & \mbox{(Lemma 17)}\\ & = ((\lambda x.PK)V)^{\sf B} & \mbox{(definition of B).} \end{align*}
If M = (λx.P)QK, M′ = (λx.PK)Q, and Q is not a value, we have
\begin{align*} ((\lambda x.P)QK)^{\sf B} & = ((\lambda x.P^{\sf B})Q^{\sf B}K^{\sf B} & \mbox{(definition of B)}\\ & \to _\sigma ((\lambda x.P^{\sf B}K^{\sf B})Q^{\sf B}\\ & \to ^*_{\beta _v} (\lambda x.(PK)^{\sf B})Q^{\sf B} & \mbox{(Lemma 17)} \\ & = ((\lambda x.PK)Q)^{\sf B} & \mbox{(definition of B).} \end{align*}
The case M = V((λx.P)Q) and M′ = (λx.VP)Q is proved similarly by Lemma 17.
Next, the induction cases are proved as follows.
If M = λx.N, M′ = λx.N′, and N→
σ
N′, by the induction hypothesis, we have
$N^{\sf B}\to ^*{N'}^{\sf B}$
. Then, we have
$(\lambda x.N)^{\sf B} = \lambda x.N^{\sf B} \to ^* \lambda{x.N'}^{\sf B} =(\lambda x.N')^{\sf B}$
.
If M = (λx.P)V, M′ = (λx.P′)V′, and either P→ σ P′ and V = V′ or V→ σ V′ and P = P′, we have
\begin{align*} ((\lambda x.P)V)^{\sf B} & =P^{\sf B}{[{x}:={{V^{\sf B}}}]} & \mbox{(definition of B)}\\ & \to ^*{P'}^{\sf B}{[{x}:={{{V'}^{\sf B}}}]} & \mbox{(induction hypothesis)}\\ & = ((\lambda x.P')V')^{\sf B} & \mbox{(definition of B).} \end{align*}
The other cases are straightforward.
The last subgoal is to prove the condition (4) of Theorem 4, that is,
$((\!\cdot \!)^{\sf S})^{\sf B}$
is weakly Z for →
β
v
by → (Proposition 20).
Lemma 19. For any terms M and M′, we have the following.
-
1. If M→ β v M′ holds, then
$M^{\sf S}\to ^*{M'}^{\sf S}$
holds.
-
2. If M→ β v M′ holds, then
$M^{\sf B}\to ^*{M'}^{\sf B}$
holds.
Proof.
-
1. By induction on a derivation of M→ β v M′. In the base case, we suppose M = (λx.P)V and M′ = P[x:=V]. We have
$((\lambda x.P)V)^{\sf S} =(\lambda x.P^{\sf S})@_3 V^{\sf S} =(\lambda x.P^{\sf S})V^{\sf S} \to _{\beta _v} P^{\sf S}{[{x}:={{V^{\sf S}}}]} \to ^*_{\beta _v} P{[{x}:={V}]}^{\sf S}$
by Lemma 16.The induction cases are proved as follows.
If M = PQ, M′ = P′Q′, P is not a value, and either P→ β v P′ and Q = Q′ or Q→ β v Q′ and P = P′, we have
$P^{\sf S}\to ^*{P'}^{\sf S}$
and
$Q^{\sf S}\to ^*{Q'}^{\sf S}$
by the induction, and then
\begin{align*} (PQ)^{\sf S} & = P^{\sf S} @_1 Q^{\sf S}\\ & \to ^*{P'}^{\sf S} @_1{Q'}^{\sf S} & \mbox{(Lemma 14)}\\ & \to ^*_\sigma (P'Q')^{\sf S} & \mbox{(Lemma 8).} \end{align*}
If P is a value, it is proved similarly.
The case λx.P→ β v λx.P′ is straightforward by the induction hypothesis.
-
2. It is straightforwardly proved by induction on a derivation of M→ β v M′, using Lemma 16.
Proposition 20.
The mapping
$((\!-\!)^{\sf S})^{\sf B}$
is weakly Z for →
β
v
by →.
Proof.
In this proof, we write
$M^{\sf SB}$
for
$(M^{\sf S})^{\sf B}$
.
First, we prove that M→
β
v
M′ implies
$M'\to ^* M^{\sf SB}$
by induction on a derivation of M→
β
v
M′.
In the base case, we suppose M = (λx.P)V and M′ = P[x:=V]. We have
$M^{\sf SB} = ((\lambda x.P^{\sf S})@_3 V^{\sf S})^{\sf B}= ((\lambda x.P^{\sf S})V^{\sf S})^{\sf B} = P^{\sf SB}{[{x}:={{V^{\sf SB}}}]}$
, and
$P{[{x}:={V}]} \to ^* P^{\sf SB}{[{x}:={{V^{\sf SB}}}]}$
holds by Lemma 10.
The induction cases are proved as follows.
If M = PQ, M = P′Q′, and either P→
β
v
P′ and Q = Q′ or Q→
β
v
Q′ and P = P′, we have
$P'\to ^* P^{\sf SB}$
and
$Q'\to ^* Q^{\sf SB}$
by the induction hypothesis and Lemma 10, and then we have
$P'Q' \to ^* P^{\sf SB}Q^{\sf SB} \to ^* (PQ)^{\sf SB}$
by Lemmas 8 and 17.
The case λx.P→ β v λx.P′ is straightforward by the induction hypothesis.
Secondly, we prove that M→
β
v
M′ implies
$M^{\sf SB}\to ^*{M'}^{\sf SB}$
. If M→
β
v
M′ holds, we have
$M^{\sf S}\to ^*{M'}^{\sf S}$
by Lemma 19 (1), and then, we have
$M^{\sf SB}\to ^*{M'}^{\sf SB}$
by Proposition 18 and Lemma 19 (2).
We have proved the conditions of Theorem 4, and hence, we give a confluence proof of λ v σ .
Theorem 21.
The mapping
$((\!-\!)^{\sf S})^{\sf B}$
is Z for → of λ
v
σ
, and hence λ
v
σ
is confluent.
Proof. It is sufficient to prove the conditions of Theorem 4. (1) is proved by Propositions 12 and 15. (2) is proved by Proposition 18. (3) is proved by Lemma 10. (4) is proved byProposition 20.
5. Conclusion
This paper gives a new proof of confluence using the compositional Z theorem for λ vσ, a variant of the call-by-value lambda calculus, which contains permutation reductions. This is a new example of an application of the compositional Z theorem. Compared with the existing proof with Hindley-Rosen’s method in Carraro and Guerrieri (Reference Carraro and Guerrieri2014), our proof does not depend on any normalization property of reduction relations.
Acknowledgements
This work was partially supported by Grants-in-Aid for Scientific Research KAKENHI 18K11161 (to Koji Nakazawa) and 17K05343 and 20K03711 (to Ken-etsu Fujita).
