-calculus and Böhm's theorem
A closed lambda term \(M\) is solvable if there exist \(M_1, \ldots ,M_n\) such that \(MM_1\ldots M_n\;\beta\)-reduces to \(I\). Böhm's Theorem states that for any two closed lambda terms \(M\) and \(N\), if for all \(N_1, \ldots ,N_k, \;MN_1, \ldots ,N_k\) is solvable if and only if \(NN_1, \ldots ,N_k\) is solvable, then \(M\) is \(\eta\)-equal to \(N\). David and Py consider this theorem for Parigot's \(\lambda \mu\)-calculus, which is \(\lambda \)-calculus extended using a \(\mu\)-operator so that the types of the terms are classical \(\neg\to\) theorems. The \(\lambda \mu\)-calculus however is not Church-Rosser when \((\eta)\) is included. This problem has been overcome by Py by including an additional reduction rule that restores the Church-Rosser property. In this paper David and Py find a counterexample to Böhm's Theorem with this form of reduction.
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
- Standardization and Böhm trees for -calculus
- The untyped stack calculus and Böhm's theorem
- Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture
- A completeness result for the simply typed \(\lambda \mu \)-calculus
- An algebraic view of the Böhm-out technique
- An analysis of Böhm's theorem
- Aharonov and Bohm versus Welsh eigenvalues
- Polarized proof-nets and \(\lambda \mu\)-calculus
- Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
- The differential \(\lambda \mu\)-calculus
- Applicative bisimilarities for call-by-name and call-by-value \(\lambda\mu\)-calculus
- Classical call-by-need and duality
- A Filter Model for the λμ-Calculus
- A Complete, Co-inductive Syntactic Theory of Sequential Control and State
- Standardization and Böhm trees for -calculus
- An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
- The relational model is injective for multiplicative exponential linear logic (without weakenings)
- scientific article; zbMATH DE number 7003195 (Why is no real title available?)
- The untyped stack calculus and Böhm's theorem
- The approximation theorem for the \(\Lambda_{\mu}\)-calculus
- Call-by-name extensionality and confluence
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Resource approximation for the -calculus
- A type-theoretic foundation of delimited continuations
This page was built for publication: \(\lambda\mu\)-calculus and Böhm's theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2732290)
