-
Effects for Efficiency: Asymptotic Speedup with First-Class Control
Authors:
Daniel Hillerström,
Sam Lindley,
John Longley
Abstract:
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language $λ_b$ and its extension with effect handlers $λ_h$. We show that $λ_h$ admits an asymptotically more efficient implementation of generic…
▽ More
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language $λ_b$ and its extension with effect handlers $λ_h$. We show that $λ_h$ admits an asymptotically more efficient implementation of generic count than any $λ_b$ implementation. We also show that this efficiency gap remains when $λ_b$ is extended with mutable state. To our knowledge this result is the first of its kind for control operators.
△ Less
Submitted 13 July, 2020; v1 submitted 1 July, 2020;
originally announced July 2020.
-
The encodability hierarchy for PCF types
Authors:
John Longley
Abstract:
Working with the simple types over a base type of natural numbers (including product types), we consider the question of when a type $σ$ is encodable as a definable retract of $τ$: that is, when there are $λ$-terms $e:σ\rightarrowτ$ and $d:τ\rightarrowσ$ with $d \circ e = id$. In general, the answer to this question may vary according to both the choice of $λ$-calculus and the notion of equality c…
▽ More
Working with the simple types over a base type of natural numbers (including product types), we consider the question of when a type $σ$ is encodable as a definable retract of $τ$: that is, when there are $λ$-terms $e:σ\rightarrowτ$ and $d:τ\rightarrowσ$ with $d \circ e = id$. In general, the answer to this question may vary according to both the choice of $λ$-calculus and the notion of equality considered; however, we shall show that the encodability relation $\preceq$ between types actually remains stable across a large class of languages and equality relations, ranging from a very basic language with infinitely many distinguishable constants $0,1,\ldots$ (but no arithmetic) considered modulo computational equality, up to the whole of Plotkin's PCF considered modulo observational equivalence. We show that $σ\preceq τ\preceq σ$ iff $σ\cong τ$ via trivial isomorphisms, and that for any $σ,τ$ we have either $σ\preceq τ$ or $τ\preceq σ$. Furthermore, we show that the induced linear order on isomorphism classes of types is actually a well-ordering of type $ε_0$, and indeed that there is a close syntactic correspondence between simple types and Cantor normal forms for ordinals below $ε_0$. This means that the relation $\preceq$ is readily decidable, and that terms witnessing a retraction $σ\lhd τ$ are readily constructible when $σ\preceq τ$ holds.
△ Less
Submitted 1 June, 2018;
originally announced June 2018.
-
Bar recursion is not computable via iteration
Authors:
John Longley
Abstract:
We show that the bar recursion operators of Spector and Kohlenbach, considered as third-order functionals acting on total arguments, are not computable in Goedel's System T plus minimization, which we show to be equivalent to a programming language with a higher-order iteration construct. The main result is formulated so as to imply the non-definability of bar recursion in T + min within a variety…
▽ More
We show that the bar recursion operators of Spector and Kohlenbach, considered as third-order functionals acting on total arguments, are not computable in Goedel's System T plus minimization, which we show to be equivalent to a programming language with a higher-order iteration construct. The main result is formulated so as to imply the non-definability of bar recursion in T + min within a variety of partial and total models, for instance the Kleene-Kreisel continuous functionals. The paper thus supplies proofs of some results stated in the book by Longley and Normann.
The proof of the main theorem makes serious use of the theory of nested sequential procedures (also known as PCF Boehm trees), and proceeds by showing that bar recursion cannot be represented by any sequential procedure within which the tree of nested function applications is well-founded.
△ Less
Submitted 19 April, 2018;
originally announced April 2018.
-
The recursion hierarchy for PCF is strict
Authors:
John Longley
Abstract:
We consider the sublanguages of Plotkin's PCF obtained by imposing some bound k on the levels of types for which fixed point operators are admitted. We show that these languages form a strict hierarchy, in the sense that a fixed point operator for a type of level k can never be defined (up to observational equivalence) using fixed point operators for lower types. This answers a question posed by B…
▽ More
We consider the sublanguages of Plotkin's PCF obtained by imposing some bound k on the levels of types for which fixed point operators are admitted. We show that these languages form a strict hierarchy, in the sense that a fixed point operator for a type of level k can never be defined (up to observational equivalence) using fixed point operators for lower types. This answers a question posed by Berger. Our proof makes substantial use of the theory of nested sequential procedures (also called PCF Böhm trees) as expounded in the recent book of Longley and Normann.
△ Less
Submitted 20 August, 2018; v1 submitted 15 July, 2016;
originally announced July 2016.
