Classical by-need

Pierre-Marie Pédrot (1, 2) , Alexis Saurin (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs

Call-by-need calculi are complex to design and reason with. When adding control effects, the very notion of canonicity is irremediably lost, the resulting calculi being necessarily ad hoc. This calls for a design of call-by-need guided by logical rather than operational considerations. Ariola et al proposed such an extension of call-by-need with control making use of Curien and Herbelin's duality of computation framework. In this paper, Classical by-need is developed as an alternative extension of call-by-need with control, better-suited for a programming-oriented reader. This method is proof-theoretically oriented by relying on linear head reduction (LHR) -- an evaluation strategy coming from linear logic -- and on the lambda-mu-calculus -- a classical extension of the lambda-calculus. More precisely, the paper contains three main contributions: - LHR is first reformulated by introducing closure contexts and extended to the lambda-mu-calculus; - it is then shown how to derive a call-by-need calculus from LHR. The result is compared with standard call-by-need calculi, namely those of Ariola--Felleisen and Chang--Felleisen; - it is finally shown how to lift the previous item to classical logic, that is from the lambda-calculus to the lambda-mu-calculus, providing a classical by-need calculus, that is a lazy lambda-mu-calculus. The result is compared with the call-by-need with control of Ariola et al.

Mots clés: call-by-need; classical logic; control operators; lambda-calculus; lambda-mu-calculus; lazy evaluation; linear head reduction; krvine abstract machine; sigma equivalence

Domaines: Logique en informatique [cs.LO]; Langage de programmation [cs.PL]

Pierre-Marie Pédrot, Alexis Saurin. Classical by-need. European Symposium on Programming, Apr 2016, Eindhoven, Netherlands. ⟨hal-01257348⟩