A short proof that adding some permutation rules to preserves SN

DOI10.1016/J.TCS.2010.10.048MaRDI QIDQ631758zbMATH OpenOpenAlexFDO

Authors René David

Publication date 14 March 2011

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1011.1335

zbMATH Keywords

lambda calculuspermutation rulesstrong normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Abstract: I show that, if a term is $SN$ for $$, it remains $SN$ when some permutation rules are added.

Recommendations

• A note on preservation of strong normalisation in the \(\lambda \)-calculus
• Short Proofs of Strong Normalization
• Explicit substitution. On the edge of strong normalization
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• scientific article; zbMATH DE number 512779

Cites work

• A Terminating and Confluent Linear Lambda Calculus
• An equivalence between lambda- terms
• Call-by-Value  -calculus and LJQ
• Delayed Substitutions
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• Normalization without reducibility
• Postponement, conservation and preservation of strong normalization for generalized reduction

Cited in

(1)

• A note on preservation of strong normalisation in the \(\lambda \)-calculus

This page was built for publication: A short proof that adding some permutation rules to \(\beta \) preserves SN

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q631758)