Advertisement
Published in:
2012 | OriginalPaper | Chapter
Call-by-Value Solvability, Revisited
Authors : Beniamino Accattoli, Luca Paolini
Published in: Functional and Logic Programming
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value-substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman’s call-by-value
λ
CBV
calculus and from Accattoli and Kesner’s substitution calculus
λ
sub
. In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.