Factoring Derivation Spaces via Intersection Types (Extended Version)

Gonzalo Ciruelos; Pablo Barenbaum

arxiv: 1907.08820 · v1 · pith:IKUVW72Knew · submitted 2019-07-20 · 💻 cs.LO

Factoring Derivation Spaces via Intersection Types (Extended Version)

Pablo Barenbaum , Gonzalo Ciruelos This is my paper

Pith reviewed 2026-05-24 18:42 UTC · model grok-4.3

classification 💻 cs.LO

keywords non-idempotent intersection typeslambda calculusderivation spacesgarbageGrothendieck constructionsimulation theoremsproof termsresource tracking

0 comments

The pith

Non-idempotent intersection types factor any lambda-calculus derivation into a garbage-free prefix followed by garbage.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a confluent non-idempotent intersection type system for the lambda-calculus, presented with proof term syntax. This system tracks resource usage in reductions and defines garbage as any computation step that does not contribute to producing an answer. Simulation theorems connect the typed system to the untyped lambda-calculus. The authors then apply a variant of the Grothendieck construction for semilattices to show that the entire space of derivations for any term admits a unique factorization into a useful prefix and subsequent garbage. A reader would care because the result supplies a canonical way to separate meaningful computation from waste inside term rewriting sequences.

Core claim

We introduce a confluent non-idempotent intersection type system for the lambda-calculus. Typing derivations are presented using proof term syntax. The system enjoys subject reduction, strong normalization, and a regular theory of residuals. A correspondence with the lambda-calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a lambda-term may be factorized using a variant of the Grothendieck建設 for

What carries the argument

The variant of the Grothendieck construction for semilattices applied to derivation spaces, induced by the notion of garbage from the confluent non-idempotent intersection type system.

If this is right

Any derivation in the lambda-calculus can be uniquely written as a garbage-free prefix followed by garbage.
Garbage is identified exactly as those steps that do not contribute to obtaining an answer under the resource-tracking types.
The factorization is obtained via a variant of the Grothendieck construction for semilattices on the derivation space.
Simulation theorems guarantee that every untyped reduction sequence lifts to a typed one and back.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Reduction strategies could be designed to detect and skip the garbage suffix once the prefix is identified.
The same resource-tracking technique might be used to measure the minimal number of steps needed to reach a normal form.
Analogous factorization results could be sought in other term-rewriting systems that admit a suitable notion of resource usage.

Load-bearing premise

The newly introduced non-idempotent intersection type system is confluent, enjoys subject reduction, strong normalization, and a regular theory of residuals.

What would settle it

A concrete lambda term together with two distinct derivations that cannot be expressed as a garbage-free prefix followed by garbage, or a pair of type reductions that produce incompatible results while preserving the same subject.

read the original abstract

In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the lambda-calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the lambda-calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a lambda-term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the lambda-calculus can be uniquely written as a garbage-free prefix followed by garbage.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a confluent non-idempotent intersection type system and applies it to factor lambda derivation spaces into garbage-free prefixes plus garbage via a semilattice construction.

read the letter

The main point is a confluent non-idempotent intersection type system for lambda calculus that supports a Grothendieck factorization of derivation spaces, writing any derivation as a garbage-free prefix followed by garbage. They set up the system using proof term syntax and prove the usual properties: subject reduction, strong normalization, and regular residuals. Simulation theorems connect it to the untyped calculus. The resource tracking then yields a garbage notion, and the factorization is obtained as a variant of the Grothendieck construction. Any derivation factors uniquely as useful prefix plus garbage. This is a useful organizational tool if the proofs go through. The work is grounded in standard techniques for intersection types. The main soft spot is the lack of proof details in the abstract, making it hard to assess how the confluence is obtained without breaking the resource counting. The central argument holds if the listed properties are established, which the paper claims they are. This paper is for researchers in resource-sensitive type systems and rewriting. A reader in that area would find the explicit factorization result of interest. It deserves a serious referee to verify the technical details. I would recommend engaging with the work through peer review.

Referee Report

2 major / 2 minor

Summary. The paper introduces a confluent non-idempotent intersection type system for the lambda-calculus, using proof-term syntax for derivations. It establishes subject reduction, strong normalization, and a regular theory of residuals, together with simulation theorems relating typed derivations to untyped lambda reductions. Resource tracking in the type system induces a notion of garbage (computations not contributing to answers). The derivation space is then factorized via a variant of the Grothendieck construction on semilattices, yielding a unique decomposition of any derivation into a garbage-free prefix followed by garbage.

Significance. If the metatheoretic results hold, the work supplies a type-theoretic mechanism for cleanly separating productive computation from garbage in lambda-calculus derivations. The combination of non-idempotent intersections with a categorical factorization construction offers a structured account of derivation spaces that may inform reduction strategies and resource analysis. The explicit use of residuals and simulation theorems to ground the garbage definition is a concrete strength.

major comments (2)

[§4] §4 (Confluence and residuals): the claim that the type system enjoys a 'very regular theory of residuals' is central to both the simulation theorems and the subsequent garbage definition; the proof that residuals commute with the typing rules must be checked for completeness, as any gap would propagate to the factorization result in §6.
[§5] §5 (Simulation theorems): the forward and backward simulation statements are load-bearing for identifying which typed steps correspond to untyped reductions; verify that the statements are stated with the precise residual relation used later to define garbage, rather than a weaker correspondence.

minor comments (2)

[Notation] The notation for proof terms (e.g., the syntax of typed derivations) should be collected in a single preliminary section or table for easier reference when reading the residual and garbage definitions.
[Figure 1] Figure 1 (or the running example of a derivation space) would benefit from explicit labels indicating which steps are classified as garbage after the factorization is applied.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and the recommendation of minor revision. The two major comments concern the completeness of the residual theory and the precision of the simulation statements; we address each directly below.

read point-by-point responses

Referee: [§4] §4 (Confluence and residuals): the claim that the type system enjoys a 'very regular theory of residuals' is central to both the simulation theorems and the subsequent garbage definition; the proof that residuals commute with the typing rules must be checked for completeness, as any gap would propagate to the factorization result in §6.

Authors: The proof that residuals commute with the typing rules is given by induction on derivation structure in the lemmas of §4 (specifically Lemmas 4.3–4.7 and the subsequent propositions establishing the residual algebra). Each case follows the standard pattern for non-idempotent intersections and is fully expanded; no steps are elided. These lemmas directly supply the residual relation used in §§5–6, so the factorization rests on a complete argument rather than an assumption. revision: no
Referee: [§5] §5 (Simulation theorems): the forward and backward simulation statements are load-bearing for identifying which typed steps correspond to untyped reductions; verify that the statements are stated with the precise residual relation used later to define garbage, rather than a weaker correspondence.

Authors: The simulation theorems (Theorems 5.1 and 5.2) are formulated with the identical residual operation defined in §4. The forward simulation preserves residuals exactly (a typed step ρ maps to an untyped step whose residuals are the images under the simulation), and the backward simulation recovers the typed residuals. Garbage is then defined as the set of steps whose residuals become empty in the final derivation; this is the same relation, not a weaker one. The text already states the correspondence in terms of the residual algebra of §4. revision: no

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper's chain proceeds by defining a new confluent non-idempotent intersection type system, proving standard metatheoretic results (subject reduction, strong normalization, regular residuals), establishing simulation theorems with the lambda-calculus, defining garbage via resource tracking, and applying a Grothendieck construction on the induced semilattice to obtain unique factorization into garbage-free prefix plus garbage. None of these steps are self-definitional, reduce a prediction to a fitted input, or rely on load-bearing self-citations whose content is unverified. The factorization result is conditional on the independently established properties rather than being equivalent to its inputs by construction. This is the normal case of a self-contained technical development in lambda-calculus and type theory.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on the existence and metatheoretic properties of the newly defined type system; the abstract invokes standard background results from lambda calculus and intersection type theory without introducing new free parameters or invented entities beyond the induced garbage notion.

axioms (2)

standard math Standard beta-reduction and subject reduction properties of the untyped lambda-calculus.
The paper builds its simulation theorems on ordinary lambda calculus reduction.
domain assumption Background results on intersection type systems and their resource-tracking capabilities.
The non-idempotent setting and the definition of garbage presuppose prior work on multiplicity tracking.

invented entities (1)

Garbage computations in typing derivations no independent evidence
purpose: To label reductions that do not contribute to obtaining a normal form or answer.
The notion is induced inside the new type system; the abstract provides no external falsifiable prediction for it.

pith-pipeline@v0.9.0 · 5687 in / 1549 out tokens · 44574 ms · 2026-05-24T18:42:42.799676+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation washburn_uniqueness_aczel echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. ... any derivation in the lambda-calculus can be uniquely written as a garbage-free prefix followed by garbage.
IndisputableMonolith/Foundation/BranchSelection branch_selection echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

the derivation space of a term is an upper semilattice ... factorized using a variant of the Grothendieck construction for semilattices

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

135 extracted references · 135 canonical work pages · 1 internal anchor

[1]

In: POPL ’14, San Diego, CA, USA, January 20-21, 201 4

Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A no nstandard standardization theorem. In: POPL ’14, San Diego, CA, USA, January 20-21, 201 4. pp. 659–670 (2014)

work page 2014
[2]

In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013

Asperti, A., L´ evy, J.: The cost of usage in the lambda-cal culus. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 293–300 (2013)

work page 2013
[3]

Information and C omputation 75(3), 191– 231 (1987)

Barendregt, H.P., Kennaway, J.R., Klop, J.W., Sleep, M.R .: Needed reduction and spine strategies for the lambda calculus. Information and C omputation 75(3), 191– 231 (1987)

work page 1987
[4]

Barendregt, H.: The Lambda Calculus: Its Syntax and Seman tics, vol. 103. Elsevier (1984)

work page 1984
[5]

Non-idempotent intersection types and strong normalisation

Bernadet, A., Lengrand, S.J.: Non-idempotent intersect ion types and strong nor- malisation. arXiv preprint arXiv:1310.1622 (2013)

work page internal anchor Pith review Pith/arXiv arXiv 2013
[6]

In : CONCUR’93

Boudol, G.: The lambda-calculus with multiplicities. In : CONCUR’93. pp. 1–6. Springer (1993) 20 P. Barenbaum and G. Ciruelos

work page 1993
[7]

In: IFIP International Con ference on Theoretical Computer Science

Bucciarelli, A., Kesner, D., Della Rocca, S.R.: The inhab itation problem for non- idempotent intersection types. In: IFIP International Con ference on Theoretical Computer Science. pp. 341–354. Springer (2014)

work page 2014
[8]

Logic Journal of the IGPL 25(4), 431–464 (2017)

Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempoten t intersection types for the lambda-calculus. Logic Journal of the IGPL 25(4), 431–464 (2017)

work page 2017
[9]

Carvalho, D.d.: S´ emantiques de la logique lin´ eaire et temps de calcul. Ph.D. thesis, Ecole Doctorale Physique et Sciences de la Mati` ere (Marsei lle) (2007)

work page 2007
[10]

Transactions of the Amer- ican Mathematical Society 39(3), 472–482 (1936)

Church, A., Rosser, J.B.: Some properties of conversion . Transactions of the Amer- ican Mathematical Society 39(3), 472–482 (1936)

work page 1936
[11]

Coppo, M., Dezani-Ciancaglini, M.: A new type assignmen t for lambda-terms. Arch. Math. Log. 19(1), 139–156 (1978)

work page 1978
[12]

Curry, H., Feys, R.: Combinatory Logic. No. v. 1 in Combin atory Logic, North- Holland Publishing Company (1958)

work page 1958
[13]

In: International Conference on Rewriting Techniques and Appl ications

Dershowitz, N., Jouannaud, J.P., Klop, J.W.: Open probl ems in rewriting. In: International Conference on Rewriting Techniques and Appl ications. pp. 445–456. Springer (1991)

work page 1991
[14]

In: LIPIcs-Leibniz In- ternational Proceedings in Informatics

Ehrhard, T.: Collapsing non-idempotent intersection t ypes. In: LIPIcs-Leibniz In- ternational Proceedings in Informatics. vol. 16. Schloss D agstuhl-Leibniz-Zentrum fuer Informatik (2012)

work page 2012
[15]

Theoretical Computer Science 309(1), 1–41 (2003)

Ehrhard, T., Regnier, L.: The diﬀerential lambda-calcu lus. Theoretical Computer Science 309(1), 1–41 (2003)

work page 2003
[16]

Theoretical Computer Science 403(2-3), 347–372 (2008)

Ehrhard, T., Regnier, L.: Uniformity and the taylor expa nsion of ordinary lambda- terms. Theoretical Computer Science 403(2-3), 347–372 (2008)

work page 2008
[17]

In: Theoretical As- pects of Computer Software

Gardner, P.: Discovering needed reductions using type t heory. In: Theoretical As- pects of Computer Software. pp. 555–574. Springer (1994)

work page 1994
[18]

Theoretical computer scien ce 50(1), 1–101 (1987)

Girard, J.Y.: Linear logic. Theoretical computer scien ce 50(1), 1–101 (1987)

work page 1987
[19]

In: International Conference on Foundations of Software Science and Computat ion Structures

Kesner, D.: Reasoning about call-by-need by means of typ es. In: International Conference on Foundations of Software Science and Computat ion Structures. pp. 424–441. Springer (2016)

work page 2016
[20]

Information and Com- putation 205(4), 419–473 (2007)

Kesner, D., Lengrand, S.: Resource operators for λ -calculus. Information and Com- putation 205(4), 419–473 (2007)

work page 2007
[21]

In: In ternational Symposium on Mathematical Foundations of Computer Science

Kesner, D., Renaud, F.: The prismoid of resources. In: In ternational Symposium on Mathematical Foundations of Computer Science. pp. 464–4 76. Springer (2009)

work page 2009
[22]

In: 21st Inter- national Conference on Foundations of Software Science and Computation Struc- tures (FoSSaCS) (2018)

Kesner, D., Ros, A., Viso, A.: Call-by-need, neededness and all that. In: 21st Inter- national Conference on Foundations of Software Science and Computation Struc- tures (FoSSaCS) (2018)

work page 2018
[23]

Kfoury, A.J.: A linearization of the lambda-calculus an d consequences. Tech. rep., Boston University Computer Science Department (1996)

work page 1996
[24]

Fundamenta Informaticae 20(4), 333–352 (1994)

Laneve, C.: Distributive evaluations of λ -calculus. Fundamenta Informaticae 20(4), 333–352 (1994)

work page 1994
[25]

L´ evy, J.J.: R´ eductions correctes et optimales dans le lambda-calcul. Ph.D. thesis, Universit´ e de Paris 7 (1978)

work page 1978
[26]

Mathematical Structures in Com- puter Science 27(5), 738–750 (2017)

L´ evy, J.J.: Redexes are stable in the λ -calculus. Mathematical Structures in Com- puter Science 27(5), 738–750 (2017)

work page 2017
[27]

Proceedings of the ACM on Programming Langua ges 2(POPL:6) (2018)

Mazza, D., Pellissier, L., Vial, P.: Polyadic approxima tions, ﬁbrations and inter- section types. Proceedings of the ACM on Programming Langua ges 2(POPL:6) (2018)

work page 2018
[28]

PhD thesis, Uni- versit´ e Paris 7 (december 1996) Factoring Derivation Spaces via Intersection Types (Exten ded Version) 21

Melli` es, P.A.: Description Abstraite des Syst` emes de R´ e´ ecriture. PhD thesis, Uni- versit´ e Paris 7 (december 1996) Factoring Derivation Spaces via Intersection Types (Exten ded Version) 21

work page 1996
[29]

In: Category Theory and Computer Science, 7th International Conference, CTCS ’97, Santa Margherita Lig- ure, Italy, September 4-6, 1997, Proceedings

Melli` es, P.: A factorisation theorem in rewriting theo ry. In: Category Theory and Computer Science, 7th International Conference, CTCS ’97, Santa Margherita Lig- ure, Italy, September 4-6, 1997, Proceedings. pp. 49–68 (19 97)

work page 1997
[30]

In: Tison, S

Melli` es, P.: Axiomatic rewriting theory VI residual th eory revisited. In: Tison, S. (ed.) Rewriting Techniques and Applications, 13th Inter national Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedin gs. Lecture Notes in Computer Science, vol. 2378, pp. 24–50. Springer (2002)

work page 2002
[31]

In: Rewrit- ing techniques and applications

Mellies, P.A.: Axiomatic rewriting theory vi: Residual theory revisited. In: Rewrit- ing techniques and applications. pp. 5–11. Springer (2002)

work page 2002
[32]

In: Processes, Terms and Cycles: Steps on the Road to Inﬁ nity, Essays Ded- icated to Jan Willem Klop, on the Occasion of His 60th Birthda y

Melli` es, P.: Axiomatic rewriting theory I: A diagramma tic standardization theo- rem. In: Processes, Terms and Cycles: Steps on the Road to Inﬁ nity, Essays Ded- icated to Jan Willem Klop, on the Occasion of His 60th Birthda y. pp. 554–638 (2005)

work page 2005
[33]

Terese: Term Rewriting Systems, Cambridge Tracts in The oretical Computer Sci- ence, vol. 55. Cambridge University Press (2003)

work page 2003
[34]

PhD thesis, Universit´ e Paris 7 (december 2017)

Vial, P.: Non-Idempotent Typing Operators, Beyond the L ambda-Calculus. PhD thesis, Universit´ e Paris 7 (december 2017)

work page 2017
[35]

Zilli, M.V.: Reduction graphs in the lambda calculus. Th eor. Comput. Sci. 29, 251–275 (1984). https://doi.org/10.1016/0304-3975(84) 90002-1 22 P. Barenbaum and G. Ciruelos A Appendix This technical appendix includes the detailed proofs of the results s tated in the main body of the paper that have been marked with the ♣ symbol. A.1 Proof of Lem. 3.6 – Su...

work page doi:10.1016/0304-3975(84 1984
[36]

By induction on t

Empty ,C = □. By induction on t. 1.1 V ariable (same), t =xA, ¯s = [s]. We have that x : [A]⊢ xA :A and ∆ ⊢ s :B are derivable, so we are done. Factoring Derivation Spaces via Intersection Types (Exten ded Version) 23 1.2 V ariable (diﬀerent), t = yA, y̸= x, ¯s = [] . We have that y : [A]⊢ yA :A is derivable, so we are done. 1.3 Abstraction, t = λ ℓy.u . ...

work page
[37]

Under an abstraction, C =λ ℓ′ y. C′. Straightforward by i.h

work page
[38]

Straightforward by i.h

Left of an application, C = C′¯u. Straightforward by i.h

work page
[39]

Straightforward by i.h

Right of an application, C =u[¯r1, C′, ¯r2]. Straightforward by i.h.. Substitution preserves correctness More precisely, let us show that if C⟨(λ ℓx.t )¯s⟩ is correct then C⟨t{ x := ¯s}⟩ is correct. By induction on C:

work page
[40]

Let ¯s = [s1,...,s n]

Empty , C = □. Let ¯s = [s1,...,s n]. Observe that if ( λ ℓx.t )[s1,...,s n] is correct then: – [c1]Γ⊕ x : [Bi]n i=1⊢ t :A and∆ i⊢ si :Bi are derivable for all i = 1..n , – [c2] t,s 1,...,s n are correct, – [c3] there are no free occurrences of x among s1,...,s n, – [c4] all the lambdas occurring in t,s 1,...,s n have pairwise distinct labels, – [c5] Γ +n...

work page
[41]

Under an abstraction, C = λ ℓ′ y. C′. Note that Γ ⊢ λ ℓ′ y. C′⟨t{ x := ¯s}⟩ : M ℓ′ →A is derivable. Let us check the three conditions to see that λ ℓ′ y. C′⟨t{ x := ¯s}⟩ is correct: 2.1 Uniquely labeled lambdas. Any two lambdas in C′⟨t{ x := ¯s}⟩ have dif- ferent labels by i.h.. We are left to check that ℓ′ does not decorate any lambda in C′⟨t{ x := ¯s}⟩....

work page
[42]

Note thatΓ ⊢ C′⟨t{ x := ¯s}⟩ : [Bj]m j=1 ℓ′ →A is derivable

Left of an application, C = C′¯u. Note thatΓ ⊢ C′⟨t{ x := ¯s}⟩ : [Bj]m j=1 ℓ′ →A is derivable. Moreover the list of arguments is of the form ¯ u = [u1,...,u m] where all the uj are correct and ∆ j⊢ uj :Bj is derivable for all j = 1..m . Then Γ +m j=1∆ j⊢ C′⟨t{ x := ¯s}⟩[uj]m j=1 :A is derivable. Let us check the three conditions to see that C′⟨t{ x := ¯s}...

work page
[43]

Similar to item 3

Right of an application, C =u[¯r1, C′, ¯r2]. Similar to item 3. Factoring Derivation Spaces via Intersection Types (Exten ded Version) 27 A.2 Proof of Lem. 3.10 – Substitution Lemma Let us prove that t{ x := ¯s}{ y := ¯u} =t{ y := ¯u1}{ x := ¯s{ y := ¯u2}} by induction on t. The interesting case is the application. Let t =r[r1,...,r n]. Then: (r[r1,...,r ...

work page
[44]

Then R :t0 = (λ ℓx.t )¯s ℓ − →# t{ x := ¯s} =t1

Empty context, C = □. Then R :t0 = (λ ℓx.t )¯s ℓ − →# t{ x := ¯s} =t1. There are two subcases, depending on whether the pattern of S is inside t or inside ¯s: 1.1 The pattern of S is in t. Using Lem. A.6, the situation is: (λ ℓx. C⟨(λ ℓ′ y.r )¯u⟩)¯s ℓ ↓↓ ℓ′ →→ (λ ℓx. C⟨r{ y := ¯u}⟩)¯s ℓ ↓↓ C⟨(λ ℓ′ y.r )¯u⟩{ x := ¯s} C⟨r{ y := ¯u}⟩{ x := ¯s} C{ x := ¯s1}⟨(...

work page
[45]

Under an abstraction, C =λ ℓ′′ y. C′. Straightforward by i.h

work page
[46]

There are three subcases, depending on whether the redex S is at the root, to the left of the application, or to the right of the application

Left of an application, C = C′¯u. There are three subcases, depending on whether the redex S is at the root, to the left of the application, or to the right of the application. 3.1 The pattern of S is at the root . Then C′⟨(λ ℓ′ x.t )¯s⟩ must have a lambda at the root, so it is of the form λ ℓ′ y. C′′′⟨(λ ℓx.t )¯s⟩. Hence, the starting term is ( λ ℓ′ y. C...

work page
[47]

Right of an application, C = r[u1,...,u i− 1, C′,u i+1,...,u n]. There are four subcases, depending on whether the redex S is at the root, to the left Factoring Derivation Spaces via Intersection Types (Exten ded Version) 29 of the application (that is, inside r), or to the right of the application (that is, either inside C′ or uj for some j). 4.1 The pat...

work page
[48]

[crI]: C⟨(λ ℓx.x A) [λ ℓ′ y.t ] ¯s⟩ → # C⟨(λ ℓ′ y.t ) ¯s⟩ → # C⟨t{{ y := ¯s}}⟩

work page
[49]

[crII]: C⟨(λ ℓx.λ ℓ′ y.t ) ¯s ¯u⟩ → # C⟨(λ ℓ′ y.t ′) ¯u⟩ → # C⟨t′{{ y := ¯u}}⟩, where t′ =t{{ x := ¯s}}

work page
[50]

C2⟨xA ¯t⟩)¯s⟩ → # C1⟨C′ 2⟨(λ ℓ′ y.u ) ¯t′⟩⟩ → # C1⟨C′ 2⟨u{{ y := ¯t′}}⟩⟩, where C2{{ x := ¯s}}= C′ 2 xA{{ x := ¯s}}=λ ℓ′ y.u ¯t{{ x := ¯s}}= ¯t′ ¯s = [ ¯s1,λ ℓ′ y.u, ¯s2] 30 P

[crIII]: C1⟨(λ ℓx. C2⟨xA ¯t⟩)¯s⟩ → # C1⟨C′ 2⟨(λ ℓ′ y.u ) ¯t′⟩⟩ → # C1⟨C′ 2⟨u{{ y := ¯t′}}⟩⟩, where C2{{ x := ¯s}}= C′ 2 xA{{ x := ¯s}}=λ ℓ′ y.u ¯t{{ x := ¯s}}= ¯t′ ¯s = [ ¯s1,λ ℓ′ y.u, ¯s2] 30 P. Barenbaum and G. Ciruelos Proof. Let R : C⟨(λ ℓx.t )¯s⟩→ # C⟨t{{ x := ¯s}}⟩be a step, and let S : C⟨t{{ x := ¯s}}⟩→ # p another step such that R creates S. The r...

work page
[51]

Then there is a two-hole context ˆC such that C = ˆC⟨□, (λ ℓ′ y.u )¯r⟩ and C1 = ˆC⟨t{{ x := ¯s}}, □⟩

If the holes of C and C1 are disjoint. Then there is a two-hole context ˆC such that C = ˆC⟨□, (λ ℓ′ y.u )¯r⟩ and C1 = ˆC⟨t{{ x := ¯s}}, □⟩. So ˆC⟨(λ ℓx.t )¯s, (λ ℓ′ y.u )¯r⟩→ # ˆC⟨t{{ x := ¯s}}, (λ ℓ′ y.u )¯r⟩→ # ˆC⟨t{{ x := ¯s}},u{{ y :=r}}⟩. Observe that S has an ancestor S0, contradicting the hypothesis that R creates S. So this case is impossible

work page
[52]

Then there exists a context C2 such that C1 = C⟨C2⟩, and we have that t{{ x := ¯s}} = C2⟨(λ ℓ′ y.u )¯r⟩

If C is a preﬁx of C1. Then there exists a context C2 such that C1 = C⟨C2⟩, and we have that t{{ x := ¯s}} = C2⟨(λ ℓ′ y.u )¯r⟩. We consider two subcases, depending on whether the position of the hole C2 lies inside the term t, or it reaches a free occurrence of x in t and “jumps” to one of the arguments in the list ¯s. 2.1 If the position of the hole of C...

work page
[53]

Then there exists a context C2 such that C = C1⟨C2⟩

If C1 is a preﬁx of C. Then there exists a context C2 such that C = C1⟨C2⟩. This means that C2⟨t{{ x := ¯s}}⟩ = (λ ℓ′ y.u )¯r. We consider three subcases, depending on whether C2 is empty, or the hole of C2 lies to the left or to the right of the application. 3.1 Empty , C2 = □. Then C = C1 so C is a preﬁx of C1. We have already considered this case. 3.2 ...

work page
[54]

Then R : (λ ℓx.t )¯s→ # t{{ x := ¯s}}

Empty context, C = □. Then R : (λ ℓx.t )¯s→ # t{{ x := ¯s}}. There are two cases for S, depending on whether it is internal to t or internal to one of the arguments of the list ¯s. 1.1 If S is internal to t. Then t = C1⟨Σ⟩ where Σ is the redex contracted byS. Let Σ ′ denote the contractum of Σ . Then: (λ ℓx. C1⟨Σ⟩) ¯s R →→ S ↓↓ C1⟨Σ⟩{{ x := ¯s}} S/R ↓↓ T ...

work page
[55]

Under an abstraction, C =λ ℓy. C′. Straightforward by i.h

work page
[56]

Let∆ be the redex contracted by R, and let∆ ′ denote its contractum

Left of an application, C = C′¯u. Let∆ be the redex contracted by R, and let∆ ′ denote its contractum. The step R is of the form C′⟨∆⟩¯u→ # C′⟨∆ ′⟩¯u. We consider three subcases, according to Creation (Lem. A.10), d epending on whether T is created by [crI], [crII], or [crIII]. 3.1 [crI] Then C′ is empty and ∆ has the following particular shape: ∆ = (λ ℓx...

work page
[57]

Let∆ be the redex contracted by R, and let∆ ′ denote its contractum

Right of an application, C =u[¯r1, C′, ¯r2]. Let∆ be the redex contracted by R, and let∆ ′ denote its contractum. The stepR is of the formu[¯r1, C′⟨∆⟩, ¯r2]→ # u[¯r1, C′⟨∆ ′⟩, ¯r2]. We consider three subcases, depending on whether the step S takes place at the root, to the left of the application, or to the righ t of the application. 4.1 If S takes place ...

work page
[58]

Note: the hypothesis that R andρ are coinitial is crucial

lab(R)∈ labs(ρ). Note: the hypothesis that R andρ are coinitial is crucial. In particular, (1) and (2) by deﬁnition only hold when R andρ are coinitial, while (3) might hold even if R and ρ are not coinitial. Proof. (1⇒ 2) Let ρ = ρ1Sσ 2 where S is a residual of R. Suppose moreover, without loss of generality, that ρ1 is minimal, i.e. thatR̸∈ ρ1. Since in...

work page
[59]

Let us show that ρ⊓ σ⊑ ρ by induction on the length of ρ

Lower bound. Let us show that ρ⊓ σ⊑ ρ by induction on the length of ρ. There are two subcases, depending on whether there is a step com mon to ρ and σ . If there is no common step, then ρ⊓ σ =ǫ trivially veriﬁes ρ⊓ σ⊑ ρ. On the other hand, if there is a common step, we have by deﬁnition th at ρ⊓ σ = R((ρ/R )⊓ (σ/R )) where R is common to ρ and σ . Recall ...

work page
[60]

Let τ be a lower bound for { ρ,σ}, i.e

Greatest lower bound. Let τ be a lower bound for { ρ,σ}, i.e. τ⊑ ρ and τ⊑ σ , and let us show that τ⊑ ρ⊓ σ . We proceed by induction on the length of ρ. There are two subcases, depending on whether there is a step common to ρ and σ . If there is no common step, we claim that τ must be empty. Otherwise we would have thatτ =Tτ ′⊑ ρ so in particular T⊑ ρ and...

work page
[61]

labs(ρ)∩ labs(σ ) = ∅

work page
[62]

Factoring Derivation Spaces via Intersection Types (Exten ded Version) 41

ρ⊓ σ =ǫ. Factoring Derivation Spaces via Intersection Types (Exten ded Version) 41

work page
[63]

In this case we say that ρ and σ are disjoint

There is no step common to ρ and σ . In this case we say that ρ and σ are disjoint. Proof. The implication (1 = ⇒ 2) is immediate since if we suppose that ρ⊓ σ is non-empty then the ﬁrst step of ρ⊓ σ is a step T such that T∈ ρ and T∈ σ . By Lem. A.14, this means that lab(T )∈ labs(ρ)∩ labs(σ ), contradicting the fact that lab(T ) and labs(ρ) are disjoint....

work page
[64]

[ρ]⊑ [σ ] implies labs(ρ)⊆ labs(σ )

Monotonic, i.e. [ρ]⊑ [σ ] implies labs(ρ)⊆ labs(σ ). By Prop. A.19

work page
[65]

Indeed, labs([ǫ]) = ∅

Preserves bottom. Indeed, labs([ǫ]) = ∅

work page
[66]

labs([ρ]⊔ [σ ]) = labs(ρ)∪ labs(σ )

Preserves joins, i.e. labs([ρ]⊔ [σ ]) = labs(ρ)∪ labs(σ ). Indeed: labs(ρ⊔ σ ) = labs(ρ(σ/ρ )) by deﬁnition of ⊔ = labs(ρ)∪ labs(σ/ρ ) = labs(ρ)∪ (labs(σ )\labs(ρ)) by Lem. A.18 = labs(ρ)∪ labs(σ )

work page
[67]

Recall that⊤ = [ρ0] where ρ0 :t ։ #∗ s is the derivation to normal form

Preserves top. Recall that⊤ = [ρ0] where ρ0 :t ։ #∗ s is the derivation to normal form. Note moreover that all derivations to normal form a re permu- tation equivalent in an orthogonal axiomatic rewrite system, so the choice does not matter. To conclude, observe that labs(ρ0) = X by deﬁnition of X, and X is indeed the top element of P(X)

work page
[68]

labs([ρ]⊓ [σ ]) = labs(ρ)∩ labs(σ )

Preserves meets, i.e. labs([ρ]⊓ [σ ]) = labs(ρ)∩ labs(σ ). We show the two inclusions: 5.1 (⊆ ) It suﬃces to check that labs(ρ⊓ σ )⊆ labs(ρ) (the inclusion labs(ρ⊓ σ )⊆ labs(σ ) is symmetric). By induction on the length of ρ⊓σ . If ρ⊓σ is empty it is immediate. If it is non-empty, ρ⊓σ =T (ρ/T ⊓σ/T ), where T is a step common to ρ andσ . Then since T is co...

work page
[69]

It suﬃces to show that labs is injective

Monomorphism. It suﬃces to show that labs is injective. Indeed, suppose that labs([ρ]) = labs([σ ]). By Coro. A.20 we have that ρ≡ σ , so [ρ] = [σ ]. A.7 Proof of Prop. 4.2 – Simulation To prove Prop. 4.2 we need an auxiliary lemma. Lemma A.23 (Reﬁnement of a substitution: composition). Ift′ ⋉ t and s′ i ⋉ s for all 1≤ i≤ n, then t′{ x := [s′ 1,...,s ′ n]...

work page
[70]

Thent = (λx.p )q→ p{ x :=q} =s andt′ is of the form (λ ℓx.p ′)[q′ 1,...,q ′ n]

Empty context, C = □. Thent = (λx.p )q→ p{ x :=q} =s andt′ is of the form (λ ℓx.p ′)[q′ 1,...,q ′ n]. We conclude by taking s′ = p′{ x := [q′ 1,...,q ′ n]}, using Lem. A.23

work page
[71]

Under an abstraction, C =λy. C′. Immediate by i.h

work page
[72]

Immediate by i.h

Left of an application, C = C′u. Immediate by i.h

work page
[73]

Then t =u C′⟨(λx.p )q⟩→ β u C′⟨p{ x := q}⟩ = s and t′ = u′[u′ 1,...,u ′ n], with u′ ⋉ u and u′ i ⋉ C′⟨(λx.p )q⟩ for all i = 1..n

Right of an application, C =uC′. Then t =u C′⟨(λx.p )q⟩→ β u C′⟨p{ x := q}⟩ = s and t′ = u′[u′ 1,...,u ′ n], with u′ ⋉ u and u′ i ⋉ C′⟨(λx.p )q⟩ for all i = 1..n . Applying the i.h. on u′ i for each i = 1..n , we have: C′⟨(λx.p )q⟩ ⋊ β →→ C′⟨p{ x :=q}⟩ ⋊ u′ i # →→ →→ u′′ i So we may conclude as follows: u C′⟨(λx.p )q⟩ ⋊ β →→ u C′⟨p{ x :=q}⟩ ⋊ u′[u′ 1,...,...

work page
[74]

Impossible

V ariablet′ =x. Impossible

work page
[75]

Abstraction, t′ =λ ℓy.r ′ Immediate by i.h

work page
[76]

There are three subcases, depending on whether the step t′→ # s′ takes place at the root, inside u′, or inside r′ i for some i = 1..n , 3.1 Reduction at the root

Application, t′ =u′[r′ 1,...,r ′ n] Then t =ur whereu′ ⋉ u andr′ i ⋉ r for all i = 1..n . There are three subcases, depending on whether the step t′→ # s′ takes place at the root, inside u′, or inside r′ i for some i = 1..n , 3.1 Reduction at the root. In this case u′ =λ ℓx.s ′. Then by Lem. A.23: (λ ℓx.s ′)[r′ 1,...,r ′ n] #↓↓ ⋉ (λx.s )r β↓↓ s′{ x := [r′...

work page
[77]

Note that t and yα 2 have the same type, namely α 2, but they do not occur at disjoint positions

The term t = (λ 1x.y α 2 )[ ] is strongly sequential. Note that t and yα 2 have the same type, namely α 2, but they do not occur at disjoint positions

work page
[78]

Note that xα 2 and yα 2 both have type α 2, but they are not simultaneously free subterms of the same subterm of t

The term t = (λ 1x.x α 2 )[yα 2 ] is strongly sequential. Note that xα 2 and yα 2 both have type α 2, but they are not simultaneously free subterms of the same subterm of t

work page
[79]

Lemma A.31 (Reﬁnement of a substitution: decomposition)

The term t =λ 1y.x [α 2] 3 → [α 2] 4 → β 5 [yα 2 ][zα 2 ] is not strongly sequential, since yα 2 andzα 2 have the same type and they are both free subterms of x[α 2] 3 → [α 2] 4 → β 5 [yα 2 ][zα 2 ]∈ sub(t). Lemma A.31 (Reﬁnement of a substitution: decomposition). If u′ ⋉ t{ x := s} and u′ is strongly sequential, then u′ is of the form t′{ x := [s′ i]n i=...

work page
[80]

Then u′ ⋉ s

V ariable (same), t = x. Then u′ ⋉ s. Let A be the type of u′. Taking t′ := xA ⋉ x we have that ( λ ℓx.x A)[u′] is strongly sequential. Regarding strong sequentiality, observe that xA and u′ have the same type, but they are not simultaneously the free subterms of any subterm of ( λ ℓx.x A)[u′]

work page

Showing first 80 references.

[1] [1]

In: POPL ’14, San Diego, CA, USA, January 20-21, 201 4

Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A no nstandard standardization theorem. In: POPL ’14, San Diego, CA, USA, January 20-21, 201 4. pp. 659–670 (2014)

work page 2014

[2] [2]

In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013

Asperti, A., L´ evy, J.: The cost of usage in the lambda-cal culus. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 293–300 (2013)

work page 2013

[3] [3]

Information and C omputation 75(3), 191– 231 (1987)

Barendregt, H.P., Kennaway, J.R., Klop, J.W., Sleep, M.R .: Needed reduction and spine strategies for the lambda calculus. Information and C omputation 75(3), 191– 231 (1987)

work page 1987

[4] [4]

Barendregt, H.: The Lambda Calculus: Its Syntax and Seman tics, vol. 103. Elsevier (1984)

work page 1984

[5] [5]

Non-idempotent intersection types and strong normalisation

Bernadet, A., Lengrand, S.J.: Non-idempotent intersect ion types and strong nor- malisation. arXiv preprint arXiv:1310.1622 (2013)

work page internal anchor Pith review Pith/arXiv arXiv 2013

[6] [6]

In : CONCUR’93

Boudol, G.: The lambda-calculus with multiplicities. In : CONCUR’93. pp. 1–6. Springer (1993) 20 P. Barenbaum and G. Ciruelos

work page 1993

[7] [7]

In: IFIP International Con ference on Theoretical Computer Science

Bucciarelli, A., Kesner, D., Della Rocca, S.R.: The inhab itation problem for non- idempotent intersection types. In: IFIP International Con ference on Theoretical Computer Science. pp. 341–354. Springer (2014)

work page 2014

[8] [8]

Logic Journal of the IGPL 25(4), 431–464 (2017)

Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempoten t intersection types for the lambda-calculus. Logic Journal of the IGPL 25(4), 431–464 (2017)

work page 2017

[9] [9]

Carvalho, D.d.: S´ emantiques de la logique lin´ eaire et temps de calcul. Ph.D. thesis, Ecole Doctorale Physique et Sciences de la Mati` ere (Marsei lle) (2007)

work page 2007

[10] [10]

Transactions of the Amer- ican Mathematical Society 39(3), 472–482 (1936)

Church, A., Rosser, J.B.: Some properties of conversion . Transactions of the Amer- ican Mathematical Society 39(3), 472–482 (1936)

work page 1936

[11] [11]

Coppo, M., Dezani-Ciancaglini, M.: A new type assignmen t for lambda-terms. Arch. Math. Log. 19(1), 139–156 (1978)

work page 1978

[12] [12]

Curry, H., Feys, R.: Combinatory Logic. No. v. 1 in Combin atory Logic, North- Holland Publishing Company (1958)

work page 1958

[13] [13]

In: International Conference on Rewriting Techniques and Appl ications

Dershowitz, N., Jouannaud, J.P., Klop, J.W.: Open probl ems in rewriting. In: International Conference on Rewriting Techniques and Appl ications. pp. 445–456. Springer (1991)

work page 1991

[14] [14]

In: LIPIcs-Leibniz In- ternational Proceedings in Informatics

Ehrhard, T.: Collapsing non-idempotent intersection t ypes. In: LIPIcs-Leibniz In- ternational Proceedings in Informatics. vol. 16. Schloss D agstuhl-Leibniz-Zentrum fuer Informatik (2012)

work page 2012

[15] [15]

Theoretical Computer Science 309(1), 1–41 (2003)

Ehrhard, T., Regnier, L.: The diﬀerential lambda-calcu lus. Theoretical Computer Science 309(1), 1–41 (2003)

work page 2003

[16] [16]

Theoretical Computer Science 403(2-3), 347–372 (2008)

Ehrhard, T., Regnier, L.: Uniformity and the taylor expa nsion of ordinary lambda- terms. Theoretical Computer Science 403(2-3), 347–372 (2008)

work page 2008

[17] [17]

In: Theoretical As- pects of Computer Software

Gardner, P.: Discovering needed reductions using type t heory. In: Theoretical As- pects of Computer Software. pp. 555–574. Springer (1994)

work page 1994

[18] [18]

Theoretical computer scien ce 50(1), 1–101 (1987)

Girard, J.Y.: Linear logic. Theoretical computer scien ce 50(1), 1–101 (1987)

work page 1987

[19] [19]

In: International Conference on Foundations of Software Science and Computat ion Structures

Kesner, D.: Reasoning about call-by-need by means of typ es. In: International Conference on Foundations of Software Science and Computat ion Structures. pp. 424–441. Springer (2016)

work page 2016

[20] [20]

Information and Com- putation 205(4), 419–473 (2007)

Kesner, D., Lengrand, S.: Resource operators for λ -calculus. Information and Com- putation 205(4), 419–473 (2007)

work page 2007

[21] [21]

In: In ternational Symposium on Mathematical Foundations of Computer Science

Kesner, D., Renaud, F.: The prismoid of resources. In: In ternational Symposium on Mathematical Foundations of Computer Science. pp. 464–4 76. Springer (2009)

work page 2009

[22] [22]

In: 21st Inter- national Conference on Foundations of Software Science and Computation Struc- tures (FoSSaCS) (2018)

Kesner, D., Ros, A., Viso, A.: Call-by-need, neededness and all that. In: 21st Inter- national Conference on Foundations of Software Science and Computation Struc- tures (FoSSaCS) (2018)

work page 2018

[23] [23]

Kfoury, A.J.: A linearization of the lambda-calculus an d consequences. Tech. rep., Boston University Computer Science Department (1996)

work page 1996

[24] [24]

Fundamenta Informaticae 20(4), 333–352 (1994)

Laneve, C.: Distributive evaluations of λ -calculus. Fundamenta Informaticae 20(4), 333–352 (1994)

work page 1994

[25] [25]

L´ evy, J.J.: R´ eductions correctes et optimales dans le lambda-calcul. Ph.D. thesis, Universit´ e de Paris 7 (1978)

work page 1978

[26] [26]

Mathematical Structures in Com- puter Science 27(5), 738–750 (2017)

L´ evy, J.J.: Redexes are stable in the λ -calculus. Mathematical Structures in Com- puter Science 27(5), 738–750 (2017)

work page 2017

[27] [27]

Proceedings of the ACM on Programming Langua ges 2(POPL:6) (2018)

Mazza, D., Pellissier, L., Vial, P.: Polyadic approxima tions, ﬁbrations and inter- section types. Proceedings of the ACM on Programming Langua ges 2(POPL:6) (2018)

work page 2018

[28] [28]

PhD thesis, Uni- versit´ e Paris 7 (december 1996) Factoring Derivation Spaces via Intersection Types (Exten ded Version) 21

Melli` es, P.A.: Description Abstraite des Syst` emes de R´ e´ ecriture. PhD thesis, Uni- versit´ e Paris 7 (december 1996) Factoring Derivation Spaces via Intersection Types (Exten ded Version) 21

work page 1996

[29] [29]

In: Category Theory and Computer Science, 7th International Conference, CTCS ’97, Santa Margherita Lig- ure, Italy, September 4-6, 1997, Proceedings

Melli` es, P.: A factorisation theorem in rewriting theo ry. In: Category Theory and Computer Science, 7th International Conference, CTCS ’97, Santa Margherita Lig- ure, Italy, September 4-6, 1997, Proceedings. pp. 49–68 (19 97)

work page 1997

[30] [30]

In: Tison, S

Melli` es, P.: Axiomatic rewriting theory VI residual th eory revisited. In: Tison, S. (ed.) Rewriting Techniques and Applications, 13th Inter national Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedin gs. Lecture Notes in Computer Science, vol. 2378, pp. 24–50. Springer (2002)

work page 2002

[31] [31]

In: Rewrit- ing techniques and applications

Mellies, P.A.: Axiomatic rewriting theory vi: Residual theory revisited. In: Rewrit- ing techniques and applications. pp. 5–11. Springer (2002)

work page 2002

[32] [32]

In: Processes, Terms and Cycles: Steps on the Road to Inﬁ nity, Essays Ded- icated to Jan Willem Klop, on the Occasion of His 60th Birthda y

Melli` es, P.: Axiomatic rewriting theory I: A diagramma tic standardization theo- rem. In: Processes, Terms and Cycles: Steps on the Road to Inﬁ nity, Essays Ded- icated to Jan Willem Klop, on the Occasion of His 60th Birthda y. pp. 554–638 (2005)

work page 2005

[33] [33]

Terese: Term Rewriting Systems, Cambridge Tracts in The oretical Computer Sci- ence, vol. 55. Cambridge University Press (2003)

work page 2003

[34] [34]

PhD thesis, Universit´ e Paris 7 (december 2017)

Vial, P.: Non-Idempotent Typing Operators, Beyond the L ambda-Calculus. PhD thesis, Universit´ e Paris 7 (december 2017)

work page 2017

[35] [35]

Zilli, M.V.: Reduction graphs in the lambda calculus. Th eor. Comput. Sci. 29, 251–275 (1984). https://doi.org/10.1016/0304-3975(84) 90002-1 22 P. Barenbaum and G. Ciruelos A Appendix This technical appendix includes the detailed proofs of the results s tated in the main body of the paper that have been marked with the ♣ symbol. A.1 Proof of Lem. 3.6 – Su...

work page doi:10.1016/0304-3975(84 1984

[36] [36]

By induction on t

Empty ,C = □. By induction on t. 1.1 V ariable (same), t =xA, ¯s = [s]. We have that x : [A]⊢ xA :A and ∆ ⊢ s :B are derivable, so we are done. Factoring Derivation Spaces via Intersection Types (Exten ded Version) 23 1.2 V ariable (diﬀerent), t = yA, y̸= x, ¯s = [] . We have that y : [A]⊢ yA :A is derivable, so we are done. 1.3 Abstraction, t = λ ℓy.u . ...

work page

[37] [37]

Under an abstraction, C =λ ℓ′ y. C′. Straightforward by i.h

work page

[38] [38]

Straightforward by i.h

Left of an application, C = C′¯u. Straightforward by i.h

work page

[39] [39]

Straightforward by i.h

Right of an application, C =u[¯r1, C′, ¯r2]. Straightforward by i.h.. Substitution preserves correctness More precisely, let us show that if C⟨(λ ℓx.t )¯s⟩ is correct then C⟨t{ x := ¯s}⟩ is correct. By induction on C:

work page

[40] [40]

Let ¯s = [s1,...,s n]

Empty , C = □. Let ¯s = [s1,...,s n]. Observe that if ( λ ℓx.t )[s1,...,s n] is correct then: – [c1]Γ⊕ x : [Bi]n i=1⊢ t :A and∆ i⊢ si :Bi are derivable for all i = 1..n , – [c2] t,s 1,...,s n are correct, – [c3] there are no free occurrences of x among s1,...,s n, – [c4] all the lambdas occurring in t,s 1,...,s n have pairwise distinct labels, – [c5] Γ +n...

work page

[41] [41]

Under an abstraction, C = λ ℓ′ y. C′. Note that Γ ⊢ λ ℓ′ y. C′⟨t{ x := ¯s}⟩ : M ℓ′ →A is derivable. Let us check the three conditions to see that λ ℓ′ y. C′⟨t{ x := ¯s}⟩ is correct: 2.1 Uniquely labeled lambdas. Any two lambdas in C′⟨t{ x := ¯s}⟩ have dif- ferent labels by i.h.. We are left to check that ℓ′ does not decorate any lambda in C′⟨t{ x := ¯s}⟩....

work page

[42] [42]

Note thatΓ ⊢ C′⟨t{ x := ¯s}⟩ : [Bj]m j=1 ℓ′ →A is derivable

Left of an application, C = C′¯u. Note thatΓ ⊢ C′⟨t{ x := ¯s}⟩ : [Bj]m j=1 ℓ′ →A is derivable. Moreover the list of arguments is of the form ¯ u = [u1,...,u m] where all the uj are correct and ∆ j⊢ uj :Bj is derivable for all j = 1..m . Then Γ +m j=1∆ j⊢ C′⟨t{ x := ¯s}⟩[uj]m j=1 :A is derivable. Let us check the three conditions to see that C′⟨t{ x := ¯s}...

work page

[43] [43]

Similar to item 3

Right of an application, C =u[¯r1, C′, ¯r2]. Similar to item 3. Factoring Derivation Spaces via Intersection Types (Exten ded Version) 27 A.2 Proof of Lem. 3.10 – Substitution Lemma Let us prove that t{ x := ¯s}{ y := ¯u} =t{ y := ¯u1}{ x := ¯s{ y := ¯u2}} by induction on t. The interesting case is the application. Let t =r[r1,...,r n]. Then: (r[r1,...,r ...

work page

[44] [44]

Then R :t0 = (λ ℓx.t )¯s ℓ − →# t{ x := ¯s} =t1

Empty context, C = □. Then R :t0 = (λ ℓx.t )¯s ℓ − →# t{ x := ¯s} =t1. There are two subcases, depending on whether the pattern of S is inside t or inside ¯s: 1.1 The pattern of S is in t. Using Lem. A.6, the situation is: (λ ℓx. C⟨(λ ℓ′ y.r )¯u⟩)¯s ℓ ↓↓ ℓ′ →→ (λ ℓx. C⟨r{ y := ¯u}⟩)¯s ℓ ↓↓ C⟨(λ ℓ′ y.r )¯u⟩{ x := ¯s} C⟨r{ y := ¯u}⟩{ x := ¯s} C{ x := ¯s1}⟨(...

work page

[45] [45]

Under an abstraction, C =λ ℓ′′ y. C′. Straightforward by i.h

work page

[46] [46]

There are three subcases, depending on whether the redex S is at the root, to the left of the application, or to the right of the application

Left of an application, C = C′¯u. There are three subcases, depending on whether the redex S is at the root, to the left of the application, or to the right of the application. 3.1 The pattern of S is at the root . Then C′⟨(λ ℓ′ x.t )¯s⟩ must have a lambda at the root, so it is of the form λ ℓ′ y. C′′′⟨(λ ℓx.t )¯s⟩. Hence, the starting term is ( λ ℓ′ y. C...

work page

[47] [47]

Right of an application, C = r[u1,...,u i− 1, C′,u i+1,...,u n]. There are four subcases, depending on whether the redex S is at the root, to the left Factoring Derivation Spaces via Intersection Types (Exten ded Version) 29 of the application (that is, inside r), or to the right of the application (that is, either inside C′ or uj for some j). 4.1 The pat...

work page

[48] [48]

[crI]: C⟨(λ ℓx.x A) [λ ℓ′ y.t ] ¯s⟩ → # C⟨(λ ℓ′ y.t ) ¯s⟩ → # C⟨t{{ y := ¯s}}⟩

work page

[49] [49]

[crII]: C⟨(λ ℓx.λ ℓ′ y.t ) ¯s ¯u⟩ → # C⟨(λ ℓ′ y.t ′) ¯u⟩ → # C⟨t′{{ y := ¯u}}⟩, where t′ =t{{ x := ¯s}}

work page

[50] [50]

C2⟨xA ¯t⟩)¯s⟩ → # C1⟨C′ 2⟨(λ ℓ′ y.u ) ¯t′⟩⟩ → # C1⟨C′ 2⟨u{{ y := ¯t′}}⟩⟩, where C2{{ x := ¯s}}= C′ 2 xA{{ x := ¯s}}=λ ℓ′ y.u ¯t{{ x := ¯s}}= ¯t′ ¯s = [ ¯s1,λ ℓ′ y.u, ¯s2] 30 P

[crIII]: C1⟨(λ ℓx. C2⟨xA ¯t⟩)¯s⟩ → # C1⟨C′ 2⟨(λ ℓ′ y.u ) ¯t′⟩⟩ → # C1⟨C′ 2⟨u{{ y := ¯t′}}⟩⟩, where C2{{ x := ¯s}}= C′ 2 xA{{ x := ¯s}}=λ ℓ′ y.u ¯t{{ x := ¯s}}= ¯t′ ¯s = [ ¯s1,λ ℓ′ y.u, ¯s2] 30 P. Barenbaum and G. Ciruelos Proof. Let R : C⟨(λ ℓx.t )¯s⟩→ # C⟨t{{ x := ¯s}}⟩be a step, and let S : C⟨t{{ x := ¯s}}⟩→ # p another step such that R creates S. The r...

work page

[51] [51]

Then there is a two-hole context ˆC such that C = ˆC⟨□, (λ ℓ′ y.u )¯r⟩ and C1 = ˆC⟨t{{ x := ¯s}}, □⟩

If the holes of C and C1 are disjoint. Then there is a two-hole context ˆC such that C = ˆC⟨□, (λ ℓ′ y.u )¯r⟩ and C1 = ˆC⟨t{{ x := ¯s}}, □⟩. So ˆC⟨(λ ℓx.t )¯s, (λ ℓ′ y.u )¯r⟩→ # ˆC⟨t{{ x := ¯s}}, (λ ℓ′ y.u )¯r⟩→ # ˆC⟨t{{ x := ¯s}},u{{ y :=r}}⟩. Observe that S has an ancestor S0, contradicting the hypothesis that R creates S. So this case is impossible

work page

[52] [52]

Then there exists a context C2 such that C1 = C⟨C2⟩, and we have that t{{ x := ¯s}} = C2⟨(λ ℓ′ y.u )¯r⟩

If C is a preﬁx of C1. Then there exists a context C2 such that C1 = C⟨C2⟩, and we have that t{{ x := ¯s}} = C2⟨(λ ℓ′ y.u )¯r⟩. We consider two subcases, depending on whether the position of the hole C2 lies inside the term t, or it reaches a free occurrence of x in t and “jumps” to one of the arguments in the list ¯s. 2.1 If the position of the hole of C...

work page

[53] [53]

Then there exists a context C2 such that C = C1⟨C2⟩

If C1 is a preﬁx of C. Then there exists a context C2 such that C = C1⟨C2⟩. This means that C2⟨t{{ x := ¯s}}⟩ = (λ ℓ′ y.u )¯r. We consider three subcases, depending on whether C2 is empty, or the hole of C2 lies to the left or to the right of the application. 3.1 Empty , C2 = □. Then C = C1 so C is a preﬁx of C1. We have already considered this case. 3.2 ...

work page

[54] [54]

Then R : (λ ℓx.t )¯s→ # t{{ x := ¯s}}

Empty context, C = □. Then R : (λ ℓx.t )¯s→ # t{{ x := ¯s}}. There are two cases for S, depending on whether it is internal to t or internal to one of the arguments of the list ¯s. 1.1 If S is internal to t. Then t = C1⟨Σ⟩ where Σ is the redex contracted byS. Let Σ ′ denote the contractum of Σ . Then: (λ ℓx. C1⟨Σ⟩) ¯s R →→ S ↓↓ C1⟨Σ⟩{{ x := ¯s}} S/R ↓↓ T ...

work page

[55] [55]

Under an abstraction, C =λ ℓy. C′. Straightforward by i.h

work page

[56] [56]

Let∆ be the redex contracted by R, and let∆ ′ denote its contractum

Left of an application, C = C′¯u. Let∆ be the redex contracted by R, and let∆ ′ denote its contractum. The step R is of the form C′⟨∆⟩¯u→ # C′⟨∆ ′⟩¯u. We consider three subcases, according to Creation (Lem. A.10), d epending on whether T is created by [crI], [crII], or [crIII]. 3.1 [crI] Then C′ is empty and ∆ has the following particular shape: ∆ = (λ ℓx...

work page

[57] [57]

Let∆ be the redex contracted by R, and let∆ ′ denote its contractum

Right of an application, C =u[¯r1, C′, ¯r2]. Let∆ be the redex contracted by R, and let∆ ′ denote its contractum. The stepR is of the formu[¯r1, C′⟨∆⟩, ¯r2]→ # u[¯r1, C′⟨∆ ′⟩, ¯r2]. We consider three subcases, depending on whether the step S takes place at the root, to the left of the application, or to the righ t of the application. 4.1 If S takes place ...

work page

[58] [58]

Note: the hypothesis that R andρ are coinitial is crucial

lab(R)∈ labs(ρ). Note: the hypothesis that R andρ are coinitial is crucial. In particular, (1) and (2) by deﬁnition only hold when R andρ are coinitial, while (3) might hold even if R and ρ are not coinitial. Proof. (1⇒ 2) Let ρ = ρ1Sσ 2 where S is a residual of R. Suppose moreover, without loss of generality, that ρ1 is minimal, i.e. thatR̸∈ ρ1. Since in...

work page

[59] [59]

Let us show that ρ⊓ σ⊑ ρ by induction on the length of ρ

Lower bound. Let us show that ρ⊓ σ⊑ ρ by induction on the length of ρ. There are two subcases, depending on whether there is a step com mon to ρ and σ . If there is no common step, then ρ⊓ σ =ǫ trivially veriﬁes ρ⊓ σ⊑ ρ. On the other hand, if there is a common step, we have by deﬁnition th at ρ⊓ σ = R((ρ/R )⊓ (σ/R )) where R is common to ρ and σ . Recall ...

work page

[60] [60]

Let τ be a lower bound for { ρ,σ}, i.e

Greatest lower bound. Let τ be a lower bound for { ρ,σ}, i.e. τ⊑ ρ and τ⊑ σ , and let us show that τ⊑ ρ⊓ σ . We proceed by induction on the length of ρ. There are two subcases, depending on whether there is a step common to ρ and σ . If there is no common step, we claim that τ must be empty. Otherwise we would have thatτ =Tτ ′⊑ ρ so in particular T⊑ ρ and...

work page

[61] [61]

labs(ρ)∩ labs(σ ) = ∅

work page

[62] [62]

Factoring Derivation Spaces via Intersection Types (Exten ded Version) 41

ρ⊓ σ =ǫ. Factoring Derivation Spaces via Intersection Types (Exten ded Version) 41

work page

[63] [63]

In this case we say that ρ and σ are disjoint

There is no step common to ρ and σ . In this case we say that ρ and σ are disjoint. Proof. The implication (1 = ⇒ 2) is immediate since if we suppose that ρ⊓ σ is non-empty then the ﬁrst step of ρ⊓ σ is a step T such that T∈ ρ and T∈ σ . By Lem. A.14, this means that lab(T )∈ labs(ρ)∩ labs(σ ), contradicting the fact that lab(T ) and labs(ρ) are disjoint....

work page

[64] [64]

[ρ]⊑ [σ ] implies labs(ρ)⊆ labs(σ )

Monotonic, i.e. [ρ]⊑ [σ ] implies labs(ρ)⊆ labs(σ ). By Prop. A.19

work page

[65] [65]

Indeed, labs([ǫ]) = ∅

Preserves bottom. Indeed, labs([ǫ]) = ∅

work page

[66] [66]

labs([ρ]⊔ [σ ]) = labs(ρ)∪ labs(σ )

Preserves joins, i.e. labs([ρ]⊔ [σ ]) = labs(ρ)∪ labs(σ ). Indeed: labs(ρ⊔ σ ) = labs(ρ(σ/ρ )) by deﬁnition of ⊔ = labs(ρ)∪ labs(σ/ρ ) = labs(ρ)∪ (labs(σ )\labs(ρ)) by Lem. A.18 = labs(ρ)∪ labs(σ )

work page

[67] [67]

Recall that⊤ = [ρ0] where ρ0 :t ։ #∗ s is the derivation to normal form

Preserves top. Recall that⊤ = [ρ0] where ρ0 :t ։ #∗ s is the derivation to normal form. Note moreover that all derivations to normal form a re permu- tation equivalent in an orthogonal axiomatic rewrite system, so the choice does not matter. To conclude, observe that labs(ρ0) = X by deﬁnition of X, and X is indeed the top element of P(X)

work page

[68] [68]

labs([ρ]⊓ [σ ]) = labs(ρ)∩ labs(σ )

Preserves meets, i.e. labs([ρ]⊓ [σ ]) = labs(ρ)∩ labs(σ ). We show the two inclusions: 5.1 (⊆ ) It suﬃces to check that labs(ρ⊓ σ )⊆ labs(ρ) (the inclusion labs(ρ⊓ σ )⊆ labs(σ ) is symmetric). By induction on the length of ρ⊓σ . If ρ⊓σ is empty it is immediate. If it is non-empty, ρ⊓σ =T (ρ/T ⊓σ/T ), where T is a step common to ρ andσ . Then since T is co...

work page

[69] [69]

It suﬃces to show that labs is injective

Monomorphism. It suﬃces to show that labs is injective. Indeed, suppose that labs([ρ]) = labs([σ ]). By Coro. A.20 we have that ρ≡ σ , so [ρ] = [σ ]. A.7 Proof of Prop. 4.2 – Simulation To prove Prop. 4.2 we need an auxiliary lemma. Lemma A.23 (Reﬁnement of a substitution: composition). Ift′ ⋉ t and s′ i ⋉ s for all 1≤ i≤ n, then t′{ x := [s′ 1,...,s ′ n]...

work page

[70] [70]

Thent = (λx.p )q→ p{ x :=q} =s andt′ is of the form (λ ℓx.p ′)[q′ 1,...,q ′ n]

Empty context, C = □. Thent = (λx.p )q→ p{ x :=q} =s andt′ is of the form (λ ℓx.p ′)[q′ 1,...,q ′ n]. We conclude by taking s′ = p′{ x := [q′ 1,...,q ′ n]}, using Lem. A.23

work page

[71] [71]

Under an abstraction, C =λy. C′. Immediate by i.h

work page

[72] [72]

Immediate by i.h

Left of an application, C = C′u. Immediate by i.h

work page

[73] [73]

Then t =u C′⟨(λx.p )q⟩→ β u C′⟨p{ x := q}⟩ = s and t′ = u′[u′ 1,...,u ′ n], with u′ ⋉ u and u′ i ⋉ C′⟨(λx.p )q⟩ for all i = 1..n

Right of an application, C =uC′. Then t =u C′⟨(λx.p )q⟩→ β u C′⟨p{ x := q}⟩ = s and t′ = u′[u′ 1,...,u ′ n], with u′ ⋉ u and u′ i ⋉ C′⟨(λx.p )q⟩ for all i = 1..n . Applying the i.h. on u′ i for each i = 1..n , we have: C′⟨(λx.p )q⟩ ⋊ β →→ C′⟨p{ x :=q}⟩ ⋊ u′ i # →→ →→ u′′ i So we may conclude as follows: u C′⟨(λx.p )q⟩ ⋊ β →→ u C′⟨p{ x :=q}⟩ ⋊ u′[u′ 1,...,...

work page

[74] [74]

Impossible

V ariablet′ =x. Impossible

work page

[75] [75]

Abstraction, t′ =λ ℓy.r ′ Immediate by i.h

work page

[76] [76]

There are three subcases, depending on whether the step t′→ # s′ takes place at the root, inside u′, or inside r′ i for some i = 1..n , 3.1 Reduction at the root

Application, t′ =u′[r′ 1,...,r ′ n] Then t =ur whereu′ ⋉ u andr′ i ⋉ r for all i = 1..n . There are three subcases, depending on whether the step t′→ # s′ takes place at the root, inside u′, or inside r′ i for some i = 1..n , 3.1 Reduction at the root. In this case u′ =λ ℓx.s ′. Then by Lem. A.23: (λ ℓx.s ′)[r′ 1,...,r ′ n] #↓↓ ⋉ (λx.s )r β↓↓ s′{ x := [r′...

work page

[77] [77]

Note that t and yα 2 have the same type, namely α 2, but they do not occur at disjoint positions

The term t = (λ 1x.y α 2 )[ ] is strongly sequential. Note that t and yα 2 have the same type, namely α 2, but they do not occur at disjoint positions

work page

[78] [78]

Note that xα 2 and yα 2 both have type α 2, but they are not simultaneously free subterms of the same subterm of t

The term t = (λ 1x.x α 2 )[yα 2 ] is strongly sequential. Note that xα 2 and yα 2 both have type α 2, but they are not simultaneously free subterms of the same subterm of t

work page

[79] [79]

Lemma A.31 (Reﬁnement of a substitution: decomposition)

The term t =λ 1y.x [α 2] 3 → [α 2] 4 → β 5 [yα 2 ][zα 2 ] is not strongly sequential, since yα 2 andzα 2 have the same type and they are both free subterms of x[α 2] 3 → [α 2] 4 → β 5 [yα 2 ][zα 2 ]∈ sub(t). Lemma A.31 (Reﬁnement of a substitution: decomposition). If u′ ⋉ t{ x := s} and u′ is strongly sequential, then u′ is of the form t′{ x := [s′ i]n i=...

work page

[80] [80]

Then u′ ⋉ s

V ariable (same), t = x. Then u′ ⋉ s. Let A be the type of u′. Taking t′ := xA ⋉ x we have that ( λ ℓx.x A)[u′] is strongly sequential. Regarding strong sequentiality, observe that xA and u′ have the same type, but they are not simultaneously the free subterms of any subterm of ( λ ℓx.x A)[u′]

work page