The Church-Rosser theorem and quantitative analysis of witnesses

DOI10.1016/j.ic.2018.09.002zbMath1436.03104OpenAlexW2892109783WikidataQ129289187 ScholiaQ129289187MaRDI QIDQ1627965

Ken-etsu Fujita

Publication date: 3 December 2018

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2018.09.002

zbMATH Keywords

lambda-calculusparallel reductionreduction strategiesGrzegorczyk hierarchyChurch-Rosser theoremGross-Knuth reduction strategyTakahashi's translationupper bounds on reduction length

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (1)

A formal system of reduction paths for parallel reduction

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Compositional Z: confluence proofs for permutative conversion
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Lectures on the Curry-Howard isomorphism
• Exact bounds for lengths of reductions in typed λ-calculus
• Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus
• Reductions of Residuals are Finite
• A Note on Shortest Developments
• Parallel reductions in \(\lambda\)-calculus
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication: The Church-Rosser theorem and quantitative analysis of witnesses