[TYPES] Typed lambda calculi with weak conversion

[Filippo Sestini]

Dear all,

Thank you for your helpful comments. I am not familiar with the suggested
references, so I will certainly give them a read.

As Gabriel said, it is not too hard to derive CH-normalization results by
looking at how other notions of reduction behave. In fact I should clarify that,
for this reason, I am more interested in literature dealing with normalization
algorithms producing weak normal forms.

I agree on your suggested connection with explicit substitutions. In fact, in
[1] the authors give a very interesting version of the weak lambda calculus
formulated with explicit subs. The translation from the original calculus to
explicit subs., called "I" in the paper, basically corresponds to your
extrusion, in that it extracts all "maximal" redexes from a term and puts them
into a substitution. Then {I(M)} = M, where {_} performs all suspended
substitutions.

Unfortunately, it seems to me that their explicit subs. calculus cannot be used
to reduce terms to weak normal form under this translation, in the sense that it
is not the case, in general, that if M normalizes to N, then I(M) normalizes to
P such that {P} = N. The reason is that beta reduction may unveil redexes that
were not there before. Under a maximal translation, this means it may ruin the
maximality property of substitutions.

Consider a term M = (lam x . (lam z . z) x) A, where A is closed and in normal
form. M has a weak normal form N = A. The maximal translation on M yields

(lam x . y x)[lam z . z/y] I(A)

and a beta contraction gives P = (y x)[lam z . z/y, I(A)/x], which is normal in
the expl. subs. calculus. However, {P} = (lam z . z) A /= A.
Of course the authors were well aware of this, as they stated the property I
referred to for single-step reductions only (Proposition 6).

Looking forward to any other comments or suggestions that you may have.

Sincerely

[1] J-J Lévy and L. Maranget, Explicit Substitutions and Programming Languages, 1999

-- 
Filippo Sestini
sestini.filippo at gmail.com
(+39) 333 6757668

> On Feb 26, 2018, at 11:38 AM, Delia Kesner <kesner at irif.fr> wrote:
> 
> Dear Filippo,
>        I've studied intersection types for weak reduction calculi
> (call by need which is a form of weak reduction and weak neededness)
> in two articles that you will find here:
> 
> https://www.irif.fr/~kesner//papers/call-by-need.pdf
> https://www.irif.fr/~kesner//papers/fossacs2018.pdf
> 
> All the best
> Delia
> 
> Le Dimanche 25 Février 2018 12:06 CET, Filippo Sestini <sestini.filippo at gmail.com> a écrit:
> 
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>> 
>> Dear all,
>> 
>> The notion of weak reduction first appeared in [1], and was later
>> developed into the definition of a weak lambda calculus in, for
>> example, [2]. The crucial property of weak reduction is that it
>> does not validate the ξ rule, but some form of computation under
>> binders is still possible.
>> 
>> I'm looking for references in the literature treating typed
>> calculi with full lambda syntax and weak conversion, in
>> particular regarding normalization. What I've found so far seems
>> to either be limited to a form of combinator syntax, or only
>> consider evaluation to weak head normal form ([3], [4]).
>> Do you have any suggestions?
>> 
>> Thank you
>> 
>> Sincerely
>> 
>> [1] W.A. Howard, Assignment of Ordinals to Terms for Primitive
>> Recursive Functionals of Finite Type, 1970
>> 1970
>> 
>> [2] N. Çağman, J.R. Hindley, Combinatory weak reduction in lambda
>> calculus, 1998
>> 
>> [3] P. Martin-Löf, An Intuitionistic Theory of Types: Predicative
>> Part, 1975
>> 
>> [4] T. Coquand, P. Dybjer, Intuitionistic Model Constructions and
>> Normalization Proofs, 1998
>> 
>> --
>> Filippo Sestini
>> sestini.filippo at gmail.com
>> (+39) 333 6757668
>> 
> 
> 
> 
> 
> 
>