Nonmodularity results for lambda calculus
A \(\lambda\)-theory is a set of equations involving closed \(\lambda\)-terms which is consistent and closed under the postulates of the \(\lambda\)-calculus. \(\lambda\)-theories form a lattice which, as the author has shown previously, is the congruence lattice of the term algebra of the least \(\lambda\)-theory \(\lambda\beta \). This term algebra generates the variety LAA of all lambda abstraction algebras. (These are purely algebraic theories of untyped lambda calculus.) In this paper the author shows that the lattice of \(\lambda\)-theories is not modular and that the variety created by the term algebra of a semisensible \(\lambda\)-theory (one where no solvable and unsolvable term are equated) is not congruence modular. Also he shows that the Mal'tsev condition for congruence modularity is inconsistent with the lambda theory generated by equating all unsolvable \(\lambda\)-terms.
- Some results on extensionality in lambda calculus
- Nondeterministic extensions of untyped \(\lambda\)-calculus
- On modular properties of higher order extensional lambda calculi
- Modal nonassociative Lambek calculus with assumptions: complexity and context-freeness
- Lambda calculus and intuitionistic linear logic
- Addition of noncombinatorial relations to the lambda calculus
- A Nominal Axiomatization of the Lambda Calculus
- On the algebraic models of lambda calculus
- Typed Lambda Calculi and Applications
- scientific article; zbMATH DE number 1508934
This page was built for publication: Nonmodularity results for lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2729668)
