Linear β-reduction

Linear head reduction is a key tool for the analysis of reduction machines for lambda-calculus and for game semantics. Its definition requires a notion of redex at a distance named primary redex in the literature. Nevertheless, a clear and complete syntactic analysis of this rule is missing. We pres...

Full description

Bibliographic Details
Main Author: Stefano Guerrini
Format: Article
Language:English
Published: Open Publishing Association 2017-01-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1701.04918v1