No solvable lambda-value term left behind
From MaRDI portal
Abstract: In the lambda calculus a term is solvable iff it is operationally relevant. Solvable terms are a superset of the terms that convert to a final result called normal form. Unsolvable terms are operationally irrelevant and can be equated without loss of consistency. There is a definition of solvability for the lambda-value calculus, called v-solvability, but it is not synonymous with operational relevance, some lambda-value normal forms are unsolvable, and unsolvables cannot be consistently equated. We provide a definition of solvability for the lambda-value calculus that does capture operational relevance and such that a consistent proof-theory can be constructed where unsolvables are equated attending to the number of arguments they take (their "order" in the jargon). The intuition is that in lambda-value the different sequentialisations of a computation can be distinguished operationally. We prove a version of the Genericity Lemma stating that unsolvable terms are generic and can be replaced by arbitrary terms of equal or greater order.
Recommendations
- scientific article; zbMATH DE number 898452
- Easy lambda-terms are not always simple
- No Eigenvalue in Finite Quantum Electrodynamics
- Lambda theories allowing terms with a finite number of fixed points
- A perturbative lambda formulation
- scientific article; zbMATH DE number 3896536
- Vacuum solutions which cannot be written in diagonal form
- scientific article; zbMATH DE number 3928339
- Lambda: The constant that refuses to die
- Autonomous Noether boundary-value problems not solved with respect to the derivative
Cited in
(12)- Every countable poset is embeddable in the poset of unsolvable terms
- Call-by-value solvability, revisited
- scientific article; zbMATH DE number 2079019 (Why is no real title available?)
- scientific article; zbMATH DE number 898452 (Why is no real title available?)
- Call-by-value Solvability
- Proving the genericity lemma by leftmost reduction is simple
- Solvability = typability + inhabitation
- Solvability for generalized applications
- Light genericity
- Meaningfulness and genericity in a subsuming framework (invited talk)
- Genericity through stratification
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
This page was built for publication: No solvable lambda-value term left behind
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5739897)
