pith. sign in

arxiv: 2606.27062 · v1 · pith:AHAPBRKAnew · submitted 2026-06-25 · 💻 cs.LO

On Jumps, Interactions, and Intersection Types

Stefano Catozi , Ugo Dal Lago , Gabriele Vanoni This is my paper

Pith reviewed 2026-06-26 02:34 UTC · model grok-4.3

classification 💻 cs.LO
keywords lambda calculusabstract machinesintersection typescost modelsjumping abstract machinegeometry of interactionnormalization complexity
0
0 comments X

The pith

The number of evaluation steps in the Parametric Jumping Abstract Machine can be extracted from a non-idempotent intersection type derivation.

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

The paper shows a tight link between a generalized version of the jumping abstract machine and non-idempotent intersection types in the lambda calculus. For any normalizing term, the exact number of steps taken by this machine follows directly from the structure of its type derivation. By setting a backtracking depth parameter to zero or leaving it free, the machine specializes to the known JAM/PAM or IAM respectively. For any fixed finite depth, the machine runs in time polynomial in the number of weak head beta reductions, yielding a reasonable cost model.

Core claim

Given a normalizing term t, the number of steps taken by the PaJAM when evaluating t can be extracted from its non-idempotent intersection type derivation. Fixing the backtracking depth recovers the JAM/PAM (depth zero) and the IAM (unconstrained depth). The PaJAM is polynomial in the number of weak head beta steps for any finite depth bound.

What carries the argument

The Parametric Jumping Abstract Machine (PaJAM) parameterized by backtracking depth, whose transitions correspond tightly to non-idempotent intersection type derivations.

If this is right

  • The JAM/PAM and IAM arise as the depth-zero and unbounded cases of the PaJAM.
  • The PaJAM provides a reasonable cost model for lambda term evaluation when the depth is bounded.
  • Step counts are directly readable from type derivations without simulating the machine.
  • Complexity bounds hold uniformly for all finite depth parameters.

Where Pith is reading between the lines

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

  • This correspondence may allow transferring complexity results between operational machines and type systems.
  • Similar parametric machines could be defined for other reduction strategies or type disciplines.
  • Bounded depth might offer practical trade-offs between precision and efficiency in evaluators.

Load-bearing premise

A tight step-exact correspondence holds between PaJAM transitions and non-idempotent intersection type derivations for normalizing terms.

What would settle it

A normalizing lambda term where the number of PaJAM steps differs from what is predicted by the size or structure of its non-idempotent intersection type derivation.

Figures

Figures reproduced from arXiv: 2606.27062 by Gabriele Vanoni, Stefano Catozi, Ugo Dal Lago.

Figure 1
Figure 1. Figure 1: As we can see from the definition, the machine relies on two mutually inductive [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original abstract

The Jumping Abstract Machine (JAM), an evaluation mechanism for the $\lambda$-calculus, was introduced by Danos and Regnier as an optimization of the Interaction Abstract Machine (IAM), itself an operational counterpart to Girard's Geometry of Interaction and Abramsky $\textit{et al}$. game semantics. Moreover, the JAM is isomorphic to the Pointer Abstract Machine (PAM), the syntactical counterpart of Hyland and Ong's game semantics. We study a generalization of the JAM, that we call the Parametric Jumping Abstract Machine (PaJAM) and show that there is a tight correspondence between the PaJAM and non-idempotent intersection types: given a normalizing term $t$, the number of steps taken by the PaJAM when evaluating $t$ can be extracted from its non-idempotent intersection type derivation. Remarkably, fixing the backtracking depth of the PaJAM, one can easily recover both the JAM/PAM, when the depth is constrained to be zero, and the IAM, when it is instead unconstrained. Exploiting type-theoretic machinery, we analyze the complexity of the PaJAM, showing that it is $\textit{polynomial}$ in the number of weak head $\beta$ steps, giving rise to a $\textit{reasonable}$ cost model, for each $\textit{finite}$ bound on the backtracking depth.

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.

Referee Report

0 major / 3 minor

Summary. The paper introduces the Parametric Jumping Abstract Machine (PaJAM) as a generalization of the JAM/PAM (depth bound zero) and IAM (unconstrained depth), parameterized by a finite backtracking depth bound. It establishes a tight, step-exact correspondence between PaJAM transitions on normalizing λ-terms and derivations in non-idempotent intersection types, from which the exact number of machine steps can be read off the type derivation. Exploiting this correspondence, the paper proves that, for any fixed finite depth bound, the PaJAM performs a number of steps polynomial in the number of weak-head β-steps, yielding a reasonable cost model.

Significance. If the claimed correspondence holds, the work supplies a uniform type-theoretic account that recovers the known JAM/PAM and IAM correspondences as special cases and extends them to a parametric family. The polynomial bound for each finite depth supplies an explicit reasonable cost model grounded in intersection-type machinery, strengthening the link between operational semantics, game semantics, and quantitative type theory.

minor comments (3)
  1. [Abstract] Abstract: the claim that the step count 'can be extracted' from the type derivation is stated without indicating the precise extraction function or the measure on derivations that yields the polynomial bound; a brief pointer to the relevant theorem would improve readability.
  2. The definition of the PaJAM transition relation (presumably in §3 or §4) should include a small worked example showing how a single backtracking step is recorded in the corresponding intersection-type derivation, to make the 'tight correspondence' concrete.
  3. Notation: the paper uses both 'depth bound' and 'backtracking depth' for the same parameter; a single consistent term and an explicit declaration of the parameter set would reduce ambiguity.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive report, accurate summary of our contributions on the PaJAM, and recommendation of minor revision. No major comments were listed in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper defines the PaJAM as a parametric generalization of the JAM/PAM/IAM and establishes a correspondence to non-idempotent intersection types, from which step counts are extracted for normalizing terms. This correspondence is derived from the machine transitions and type rules rather than reducing by construction to fitted inputs or self-definitions. The polynomial bound for finite depth follows from the type-theoretic analysis. No load-bearing self-citation, uniqueness theorem imported from authors, or renaming of known results is required for the central claim; the construction is independent of the target quantities.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 1 invented entities

Only the abstract is available, so the ledger is necessarily incomplete. The central claim rests on the existence of a correspondence between machine transitions and type derivations plus standard background results in lambda calculus and intersection types.

free parameters (1)
  • backtracking depth bound
    Finite integer bound on backtracking depth; required for the polynomial complexity claim and for recovering JAM (bound 0) versus IAM (unbounded).
axioms (1)
  • standard math Standard properties of the lambda calculus, weak-head beta reduction, and non-idempotent intersection types hold as previously established in the literature.
    Invoked when stating that the PaJAM step count can be extracted from a type derivation for normalizing terms.
invented entities (1)
  • Parametric Jumping Abstract Machine (PaJAM) no independent evidence
    purpose: Generalization of JAM that adds a tunable backtracking depth parameter.
    New machine introduced in the paper; no independent evidence outside the definitions given.

pith-pipeline@v0.9.1-grok · 5771 in / 1530 out tokens · 22574 ms · 2026-06-26T02:34:13.540825+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

244 extracted references · 59 canonical work pages

  1. [1]

    Steffen van Bakel , title =. Theor. Comput. Sci. , volume =. 1992 , url =. doi:10.1016/0304-3975(92)90297-S , timestamp =

    work page doi:10.1016/0304-3975(92)90297-s 1992

  2. [2]

    Beniamino Accattoli and Dal Lago, Ugo and Gabriele Vanoni , title =. Proc. 2022 , url =. doi:10.1145/3547650 , timestamp =

    work page doi:10.1145/3547650 2022

  3. [3]

    Pierre Vial , editor =. Every. Proceedings of the 33rd Annual. 2018 , url =. doi:10.1145/3209108.3209133 , timestamp =

    work page doi:10.1145/3209108.3209133 2018

  4. [5]

    Antonio Bucciarelli and Thomas Ehrhard , title =. Ann. Pure Appl. Log. , volume =. 2001 , url =. doi:10.1016/S0168-0072(00)00056-7 , timestamp =

    work page doi:10.1016/s0168-0072(00)00056-7 2001

  5. [6]

    Antonio Bucciarelli and Delia Kesner and Daniel Ventura , title =. Log. J. 2017 , url =. doi:10.1093/JIGPAL/JZX018 , timestamp =

    work page doi:10.1093/jigpal/jzx018 2017

  6. [7]

    Generalised species of rigid resource terms , booktitle =

    Takeshi Tsukada and Kazuyuki Asada and C. Generalised species of rigid resource terms , booktitle =. 2017 , url =. doi:10.1109/LICS.2017.8005093 , timestamp =

    work page doi:10.1109/lics.2017.8005093 2017

  7. [8]

    Damiano Mazza and Luc Pellissier and Pierre Vial , title =. Proc. 2018 , url =. doi:10.1145/3158094 , timestamp =

    work page doi:10.1145/3158094 2018

  8. [10]

    Moore, E. H. and Smith, H. L. , year =. A General Theory of Limits , volume =. American Journal of Mathematics , publisher =. doi:10.2307/2370388 , number =

    work page doi:10.2307/2370388

  9. [11]

    3): semantic structures , year =

    Handbook of logic in computer science (vol. 3): semantic structures , year =

  10. [12]

    Linear Logic , journal =

    Jean. Linear Logic , journal =. 1987 , url =. doi:10.1016/0304-3975(87)90045-4 , timestamp =

    work page doi:10.1016/0304-3975(87)90045-4 1987

  11. [14]

    Scott , title =

    Dana S. Scott , title =. Toposes, Algebraic Geometry and Logic , pages =. 1972 , doi =

    1972

  12. [15]

    Algebras and combinators , volume =

    Engeler, Erwin , year =. Algebras and combinators , volume =. Algebra Universalis , publisher =. doi:10.1007/bf02483849 , number =

    work page doi:10.1007/bf02483849

  13. [16]

    Plotkin , title =

    Gordon D. Plotkin , title =. Theor. Comput. Sci. , volume =. 1993 , url =. doi:10.1016/0304-3975(93)90094-A , timestamp =

    work page doi:10.1016/0304-3975(93)90094-a 1993

  14. [17]

    The lambda calculus: its syntax and semantics , isbn =

    Barendregt, Hendrik Pieter , year =. The lambda calculus: its syntax and semantics , isbn =

  15. [18]

    Réductions correctes et optimales dans le lambda-calcul , school =

    Lévy, Jean-Jacques , year =. Réductions correctes et optimales dans le lambda-calcul , school =

  16. [19]

    Gonthier, Georges and Abadi, Martín and Lévy, Jean-Jacques , year =. The. Proceedings of the 19th

  17. [20]

    Theoretical Computer Science , author =

    Linear logic , volume =. Theoretical Computer Science , author =. 1987 , pages =

    1987

  18. [21]

    Geometry of Interaction 1: Interpretation of System F

    Jean-Yves Girard. Geometry of Interaction 1: Interpretation of System F. Logic Colloquium '88. 1989. doi:https://doi.org/10.1016/S0049-237X(08)70271-4

    work page doi:10.1016/s0049-237x(08)70271-4 1989

  19. [22]

    Theoretical Computer Science , author =

    Reversible, irreversible and optimal lambda-machines , volume =. Theoretical Computer Science , author =. doi:10.1016/S0304-3975(99)00049-3 , year =

    work page doi:10.1016/s0304-3975(99)00049-3

  20. [23]

    arXiv:1803.00427 [cs] , author =

    The. arXiv:1803.00427 [cs] , author =. 2018 , keywords =

    arXiv 2018

  21. [24]

    Logical Methods in Computer Science , author =

    (. Logical Methods in Computer Science , author =. doi:10.2168/LMCS-12(1:4)2016 , year =

    work page doi:10.2168/lmcs-12(1:4)2016 2016

  22. [25]

    Conference Record of POPL'95: 22nd

    Ian Mackie , title =. Conference Record of POPL'95: 22nd. 1995 , doi =

    1995

  23. [26]

    Higher Order Symbol

    A. Higher Order Symbol. Comput. , author =. 2007 , doi =

    2007

  24. [27]

    Information and Computation , author =

    New. Information and Computation , author =. 1994 , pages =

    1994

  25. [28]

    Mathematical Structures in Computer Science , author =

    Geometry of. Mathematical Structures in Computer Science , author =. 2002 , pages =

    2002

  26. [29]

    Ghica , title =

    Dan R. Ghica , title =. Proceedings of the 34th. 2007 , doi =

    2007

  27. [30]

    Ghica and Alex I

    Dan R. Ghica and Alex I. Smith , title =. Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics,. 2010 , doi =

    2010

  28. [31]

    Information and Computation , author =

    Computation by interaction for space-bounded functional programming , volume =. Information and Computation , author =. 2016 , keywords =

    2016

  29. [32]

    Tight. Proc. ACM Program. Lang. , author =. 2018 , keywords =

    2018

  30. [33]

    Andrea Asperti and Cosimo Laneve , title =. Theor. Comput. Sci. , volume =. 1995 , timestamp =

    1995

  31. [34]

    Proceedings, 11th Annual

    Vincent Danos and Hugo Herbelin and Laurent Regnier , title =. Proceedings, 11th Annual. 1996 , doi =

    1996

  32. [35]

    , year =

    Felleisen, Matthias and Friedman, Daniel P. , year =. Control operators, the. 3rd

  33. [36]

    Proceedings of the Eighth Annual Symposium on Logic in Computer Science

    Vincent Danos and Laurent Regnier , title =. Proceedings of the Eighth Annual Symposium on Logic in Computer Science. 1993 , doi =

    1993

  34. [37]

    Memoryful geometry of interaction: from coalgebraic components to algebraic effects , booktitle =

    Naohiko Hoshino and Koko Muroya and Ichiro Hasuo , editor =. Memoryful geometry of interaction: from coalgebraic components to algebraic effects , booktitle =. 2014 , doi =

    2014

  35. [38]

    Proceedings of

    Beniamino Accattoli , title =. Proceedings of. 2012 , pages =

    2012

  36. [39]

    Electronic Notes in Theoretical Computer Science , volume =

    Robin Milner , title =. Electronic Notes in Theoretical Computer Science , volume =. 2007 , pages =

    2007

  37. [40]

    Milner's Lambda Calculus with Partial Substitutions , year =

    Delia Kesner and Shane. Milner's Lambda Calculus with Partial Substitutions , year =

  38. [41]

    Proceedings of CSL'10 , year =

    Beniamino Accattoli and Delia Kesner , title =. Proceedings of CSL'10 , year =

  39. [42]

    Proceedings of the 15th ICTAC , pages =

    Beniamino Accattoli , title =. Proceedings of the 15th ICTAC , pages =. 2018 , timestamp =

    2018

  40. [43]

    Distilling abstract machines , booktitle =

    Beniamino Accattoli and Pablo Barenbaum and Damiano Mazza , editor =. Distilling abstract machines , booktitle =. 2014 , doi =

    2014

  41. [44]

    Beniamino Accattoli and Giulio Guerrieri , title =. Sci. Comput. Program. , volume =. 2019 , url =. doi:10.1016/j.scico.2019.03.002 , timestamp =

    work page doi:10.1016/j.scico.2019.03.002 2019

  42. [45]

    Damiano Mazza and Luc Pellissier and Pierre Vial , title =. Proc. 2018 , doi =

    2018

  43. [46]

    Crumbling Abstract Machines , booktitle =

    Beniamino Accattoli and Andrea Condoluci and Giulio Guerrieri and Sacerdoti Coen, Claudio , editor =. Crumbling Abstract Machines , booktitle =. 2019 , doi =

    2019

  44. [47]

    Environments and the complexity of abstract machines , booktitle =

    Beniamino Accattoli and Bruno Barras , editor =. Environments and the complexity of abstract machines , booktitle =. 2017 , doi =

    2017

  45. [48]

    Parsimonious Types and Non-uniform Computation , booktitle =

    Damiano Mazza and Kazushige Terui , editor =. Parsimonious Types and Non-uniform Computation , booktitle =. 2015 , doi =

    2015

  46. [49]

    The geometry of synchronization , booktitle =

    Dal Lago, Ugo and Claudia Faggian and Ichiro Hasuo and Akira Yoshimizu , editor =. The geometry of synchronization , booktitle =. 2014 , doi =

    2014

  47. [50]

    Parallelism and Synchronization in an Infinitary Context , booktitle =

    Dal Lago, Ugo and Claudia Faggian and Beno. Parallelism and Synchronization in an Infinitary Context , booktitle =. 2015 , doi =

    2015

  48. [51]

    32nd Annual

    Dal Lago, Ugo and Ryo Tanaka and Akira Yoshimizu , title =. 32nd Annual. 2017 , doi =

    2017

  49. [52]

    23rd International Conference on Rewriting Techniques and Applications (RTA'12) ,

    Beniamino Accattoli and Dal Lago, Ugo , title =. 23rd International Conference on Rewriting Techniques and Applications (RTA'12) ,. 2012 , doi =

    2012

  50. [53]

    Simple Parsimonious Types and Logarithmic Space , booktitle =

    Damiano Mazza , editor =. Simple Parsimonious Types and Logarithmic Space , booktitle =. 2015 , doi =

    2015

  51. [54]

    The geometry of parallelism: classical, probabilistic, and quantum effects , booktitle =

    Dal Lago,Ugo and Claudia Faggian and Beno. The geometry of parallelism: classical, probabilistic, and quantum effects , booktitle =. 2017 , timestamp =

    2017

  52. [55]

    Blelloch and John Greiner , title =

    Guy E. Blelloch and John Greiner , title =. Proceedings of the seventh international conference on Functional programming languages and computer architecture,. 1995 , doi =

    1995

  53. [56]

    Lambda Calculi and Linear Speedups , booktitle =

    David Sands and J. Lambda Calculi and Linear Speedups , booktitle =. 2002 , doi =

    2002

  54. [57]

    Call-by-Value lambda-Graph Rewriting Without Rewriting , booktitle =

    Maribel Fern. Call-by-Value lambda-Graph Rewriting Without Rewriting , booktitle =. 2002 , doi =

    2002

  55. [58]

    A Geometry of Interaction Machine for G

    Ian Mackie , editor =. A Geometry of Interaction Machine for G. Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings , series =. 2017 , doi =

    2017

  56. [59]

    Abstract machines for dialogue games , year =

    Pierre. Abstract machines for dialogue games , year =

  57. [60]

    Computing with Abstract B

    Pierre. Computing with Abstract B. Third Fuji International Symposium on Functional and Logic Programming,. 1998 , timestamp =

    1998

  58. [61]

    A Token Machine for Full Geometry of Interaction , booktitle =

    Olivier Laurent , editor =. A Token Machine for Full Geometry of Interaction , booktitle =. 2001 , doi =

    2001

  59. [62]

    Proceedings of the Ninth Annual Symposium on Logic in Computer Science

    Andrea Asperti and Vincent Danos and Cosimo Laneve and Laurent Regnier , title =. Proceedings of the Ninth Annual Symposium on Logic in Computer Science. 1994 , doi =

    1994

  60. [63]

    Dal Lago, Ugo and Simone Martini , title =. Theor. Comput. Sci. , volume =. 2008 , timestamp =

    2008

  61. [64]

    12th Workshop on Logical and Semantic Frameworks, with Applications,

    Beniamino Accattoli , title =. 12th Workshop on Logical and Semantic Frameworks, with Applications,. 2017 , doi =

    2017

  62. [65]

    Proceedings of the 30th

    Beniamino Accattoli and Sacerdoti Coen, Claudio , title =. Proceedings of the 30th. 2015 , timestamp =

    2015

  63. [66]

    Proceedings of the 7th

    Beniamino Accattoli , title =. Proceedings of the 7th. 2013 , timestamp =

    2013

  64. [67]

    1996 , timestamp =

    David Sands , title =. 1996 , timestamp =

    1996

  65. [68]

    Une équivalence sur les lambda- termes

    Laurent Regnier. Une équivalence sur les lambda- termes. Theoretical Computer Science. 1994

    1994

  66. [69]

    2020 , note=

    The Abstract Machinery of Interaction (Long Version) , author=. 2020 , note=

    2020

  67. [70]

    On the Relation of Interaction Semantics to Continuations and Defunctionalization , journal =

    Ulrich Sch. On the Relation of Interaction Semantics to Continuations and Defunctionalization , journal =. 2014 , doi =

    2014

  68. [71]

    From Call-by-Value to Interaction by Typed Closure Conversion , booktitle =

    Ulrich Sch. From Call-by-Value to Interaction by Typed Closure Conversion , booktitle =. 2015 , doi =

    2015

  69. [72]

    Traced monoidal categories , volume=

    Joyal, André and Street, Ross and Verity, Dominic , year=. Traced monoidal categories , volume=. Mathematical Proceedings of the Cambridge Philosophical Society , publisher=

  70. [73]

    Damiano Mazza , title =

  71. [74]

    Stratified Bounded Affine Logic for Logarithmic Space , booktitle =

    Ulrich Sch. Stratified Bounded Affine Logic for Logarithmic Space , booktitle =. 2007 , doi =

    2007

  72. [75]

    Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming , articleno =

    Accattoli, Beniamino and Dal Lago, Ugo and Vanoni, Gabriele , title =. Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming , articleno =. 2020 , isbn =. doi:10.1145/3414080.3414108 , abstract =

    work page doi:10.1145/3414080.3414108 2020

  73. [76]

    Proceedings of the Workshop on Advances in Linear Logic , pages =

    Danos, Vincent and Regnier, Laurent , title =. Proceedings of the Workshop on Advances in Linear Logic , pages =. 1995 , isbn =

    1995

  74. [77]

    J. M. E. Hyland and C. On Full Abstraction for. Inf. Comput. , volume =. 2000 , doi =

    2000

  75. [78]

    Samson Abramsky and Radha Jagadeesan and Pasquale Malacaria , title =. Inf. Comput. , volume =. 2000 , doi =

    2000

  76. [79]

    Functional Programming in Sublinear Space , booktitle =

    Dal Lago, Ugo and Ulrich Sch. Functional Programming in Sublinear Space , booktitle =. 2010 , doi =

    2010

  77. [80]

    Krishnaswami and Nick Benton and Jan Hoffmann , title =

    Neelakantan R. Krishnaswami and Nick Benton and Jan Hoffmann , title =. Proc. of. 2012 , doi =

    2012

  78. [81]

    Ghica , title =

    Koko Muroya and Dan R. Ghica , title =. 26th. 2017 , doi =

    2017

  79. [82]

    Ghica , title =

    Koko Muroya and Dan R. Ghica , title =. Log. Methods Comput. Sci. , volume =. 2019 , url =

    2019

  80. [83]

    Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction , booktitle =

    Jorge Sousa Pinto , editor =. Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction , booktitle =. 2001 , url =. doi:10.1007/3-540-45413-6\_30 , timestamp =

    work page doi:10.1007/3-540-45413-6 2001

Showing first 80 references.