Titulo:
An Operational Characterization of (Lazy)-Strong Normalization
Abstract:
The standard lambda-calculus equipped with the beta-reduction
is the language for the call-by-name functional
computation. Its call-by-value version is the well known
Plotkin's lambda-Bv-calculus.
In this work, we use the parametric lambda-Delta-calculus
in order to present a logical characterization of
lazy strongly beta-normalizing terms using intersection types.
This characterization, besides being interesting by itself, allows
an interesting connection between call-by-name and call-by-value
lambda-calculus.
In fact, it turns out that the class of lazy strongly
beta-normalizing terms coincides with that of call-by-value potentially
valuable terms. This last class is of particular interest since it
is a key notion for characterizing solvability in the
call-by-value setting.
We also introduce the Phi-calculus, a new call-by-value
version of the lambda-calculus. The Phi-calculus
satisfies some interesting properties, in particular that its set of
solvable terms coincides with the set of beta-strongly
normalizing terms in the classical lambda-calculus.