RUS  ENG
Full version
JOURNALS // Computing, Telecommunication and Control // Archive

St. Petersburg Polytechnical University Journal. Computer Science. Telecommunication and Control Sys, 2017 Volume 10, Issue 3, Pages 59–82 (Mi ntitu184)

Software of Computer, Telecommunications and Control Systems

Complete head linear reduction

D. A. Berezun

Saint Petersburg State University

Abstract: n lambda calculus, head linear reduction is a reduction strategy which reaches a quasi-head normal form of terms in the minimum number of linear substitution steps. The paper is dedicated to the generalization of head linear reduction to a complete head linear reduction which yields normal forms when they exist. The formal presentation of both head linear reduction and complete head linear reduction via transition systems is provided. We also proved that both reduction strategies are correct: head linear reduction with respect to head reduction, i.e., that head linear reduction terminates in quasi-head normal form if and only if head reduction terminates, and we proved that complete head linear reduction is an effective reduction strategy, i.e., it terminates if and only if the normal form exists.

Keywords: lambda-calculus, reduction strategy, linear reduction, head linear reduction, complete head linear reduction, traversal-based normalization.

UDC: 519.682.1

DOI: 10.18721/JCSTCS.10306



© Steklov Math. Inst. of RAS, 2024