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.
From: Gabriele Vanoni [view email]
[v1]
Thu, 25 Jun 2026 14:07:22 UTC (516 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。