Termination of lambda-calculus with the extra Call-By-Value rule known as assoc

TL;DR

This paper proves that lambda-terms strongly normalising under beta-reduction are also strongly normalising under an extended call-by-value rule called assoc, providing a complete and rigorous proof for this property.

Contribution

It offers the first complete proof that strongly normalising lambda-terms remain so under the assoc call-by-value rule, clarifying a previously uncertain theoretical result.

Findings

Strong normalisation is preserved under beta,assoc-reduction.

Provides a rigorous proof filling gaps in prior work.

Confirms the theoretical consistency of assoc in lambda calculus.

Abstract

In this paper we prove that any lambda-term that is strongly normalising for beta-reduction is also strongly normalising for beta,assoc-reduction. assoc is a call-by-value rule that has been used in works by Moggi, Joachimsky, Espirito Santo and others. The result has often been justified with incomplete or incorrect proofs. Here we give one in full details.