Dynamic GoI machines

Talk by Koko Muroya (University of Birmingham)
Time: 14:30-14:45
Slides

Abstract

Girard’s Geometry of Interaction is known to give an interpretation of lambda-calculus as an abstract machine in which a token computes a value by travelling around a proof net. Danos and Regnier prove that their Interaction Abstract Machine can correspond to the Krivine abstract machine and hence implement the call-by-name evaluation strategy. Since then it has been a challenge to implement the call-by-value evaluation strategy by means of GoI-based abstract machines. Difficulties lie on both the order and cost of evaluation. A GoI-based abstract machine naturally postpones, repeats, or even neglect the evaluation of function arguments. Some previous attempts include: use of the CPS transformation by Hoshino et al. and Schoepp, and use of parallelism by Dal Lago et al. They prevent postponing and neglecting the evaluation of function arguments, and therefore achieve adequacy for the call-by-value evaluation strategy. However re-evaluation of function arguments has not been fully ruled out.

In this progress report we first introduce a variant of GoI-based abstract machine that dynamically rewrites an underlying proof net during its execution. Each rewrite is triggered by a token, i.e. a redex is detected using a path the token followed so far. This abstract machine just excludes re-evaluation of function arguments, and therefore would implement the call-by-need evaluation strategy. We also mention our attempt to implement the call-by-value evaluation strategy, in which our abstract machine is not any more allowed to postpone, repeat nor neglect the evaluation of a function argument. This attempt will lead to a GoI-based abstract machine that has a great opportunity to safely accommodate computational effects.