Head Linear Reduction
Vincent Danos, Laurent Régnier · 2004
This paper defines head linear reduction, a reduction strategy of #-terms that performs the minimal number of substitutions for reaching a head normal form. The definition relies on an extended notion of redex, and head linear reduction is therefore not a strategy in the exact usual sense. Krivine 's Abstract Machine is proved to be sound by relating it both to head linear reduction and to usual head reduction. The first proof suggests a variant machine, the Pointer Abstract Machine, which is also proved to be sound with respect to head linear reduction.