
VOLUME 12, ISSUE 2, PAPER 12
No solvable lambdavalue term left behind

©Álvaro GarcíaPérez, Reykjavík University, Iceland ©Pablo Nogueira, IMDEA Software Institute, Madrid, Spain 
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 lambdavalue calculus, called vsolvability, but it is not synonymous with
operational relevance, some lambdavalue normal forms are unsolvable, and
unsolvables cannot be consistently equated. We provide a definition of
solvability for the lambdavalue calculus that does capture operational
relevance and such that a consistent prooftheory 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 lambdavalue 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.

Publication date: June 30, 2016
Full Text: PDF  PostScript DOI: 10.2168/LMCS12(2:12)2016
Hit Counts: 2513 
Creative Commons  