Re: [TYPES] Typed lambda calculi with weak conversion

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Filippo, dear Gabriel,

One reason the Çağman and Hindley's notion of weak reduction is appreciated might be that it makes the weak lambda-calculus behave exactly like an orthogonal first-order term rewriting system (which basically means ‘simple and nicely confluent’).
In particular it does never hide a redex, like in a term

  (\xy.x)((\lz.z) a)

that would be reduced in normal order reduction to a weak normal form

  \y.((\z.z) a)

where the redex that was once visible in the argument is now hidden.
I assume when you speak of ‘normalization’ you mean ‘strong normalization’, that is requiring that any reduction strategy reaches a normal form (in contrast to ‘weak normalization’ that only requires the existence of one -potentially non-computable- normalizing strategy). Otherwise both variants of weak reduction will definitely be different.

One proof of the equivalence is in Sec. 4 of this paper:
https://www.lri.fr/~blsk/Docs/Balabonski-FullLaziness-POPL12.pdf


Regarding the ‘extrusion’ transformation, this looks really similar to the hoisting of maximal free expressions. The transformation is present in the usual presentation of fully lazy lambda-lifting (see SPJ’s The Implementation of Functional Programming Languages). It is also presented as a program transformation that implements fully lazy reduction using a ‘simply lazy’ evaluation mechanism (see Ariola and Felleisen’s JFP version of the call-by-need lambda-calculus).

Thibaut.



> Le 25 févr. 2018 à 16:34, Gabriel Scherer <[email protected]> a écrit :
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> # Çağman and Hindley's notion of weak reduction
> 
> For those that would not be familiar with the work of Çağman and Hindley,
> 1998 (it is a nice paper that is still readable today, so don't hesitate to
> have a look), they give a definition of weak reduction (as opposed to
> strong/full reduction) that is a bit stronger (and arguably better-behaved)
> than the standard one: instead of saying "don't reduce under lambdas", they
> say "only reduce closed term" -- this is essentially the same thing, except
> that they allow themselves to reduce closed sub-terms that would occur
> under a lambda. For example:
> 
>  (lam y. (lam x. x) (lam z. z))
> 
> would not reduce for the common notion of weak reduction ((lam y . []) is
> not an evaluation context), but it does reduce to
> 
>  (lam y. (lam z. z))
> 
> for their notion of weak reduction. (Luc Maranget once claimed to me that
> this is the "right" notion of weak reduction.)
> 
> One nice idea in the paper of Çağman and Hindley is that this can be
> characterized very nicely by using the no-variable-capture property of
> substitutions (as opposed to context plugging). Strong/full reduction can
> be defined by saying that, for any head-reduction from A to B (a "head"
> reduction is when A is the redex, instead of merely containing the redex as
> a subterm; if you only have functions, this is when A is of the form ((lam
> x. C) D)):
> 
>  C[A] reduces to C[B]
> 
> for an arbitrary context C. (Just a term with a hole, no particular
> restriction to a family of evaluation contexts). Çağman and Hindley remark
> that their notion of weak reduction can be characterized by saying that,
> for any head-reduction from A to B,
> 
>  C[A/x] reduces to C[B/x]
> 
> using (capture-avoiding) substitution instead of context plugging imposes
> that A and B do not contain a variable bound in C, which precisely
> corresponds to their notion of weak reduction.
> (Consider (lam y . z) and (lam y . y), the former can be written as (lam y
> . x)[z/x], but the latter is not equal to (lam y . x)[y/x].)
> 
> # Normalization of weak reduction
> 
> To answer Filippo's question: I don't think that enlarging the notion of
> weak reduction to reduce closed subterms changes the normalization behavior
> in any way: the two notions of weak reduction have the same normalization
> properties.
> 
> In particular, consider a term of the form
> 
>  C[A]
> 
> where A is a closed sub-term in the sense that is under some lambdas in C,
> but does not use their bound variables. A is not reducible under the
> no-reduction-under-lambda interpretation (the common one), but it is
> reducible under the reduce-closed-subterms interpretation (Çağman and
> Hindley's -- let's call it "CH weak reduction" for short). But this term is
> beta-equivalent to
> 
>  (lam x. C[x]) A
> 
> where A is in reducible position under either notions of reductions. If
> C[A] was non-normalizable for CH weak reduction, then ((lam x. C[x]) A) is
> non-normalizable for standard weak reduction. If the standard calculus has
> a weak-normalization property, then you know that Ch-reducing A in C[A]
> preserves normalization.
> 
> My intuition suggests that this can be turned a general construction that
> extrudes all closed sub-term of a term, and produces from any term T an
> extruded term T' such that the CH-weak normal form of T is the standard
> normal form of T'. (Of course, this is only intuition, one has to do the
> work.) (This extrusion is type-preserving.) This means that any
> normalization result for standard weak reduction implies a normalization
> result for CH weak reduction.
> 
> 
> # Explicit substitutions
> 
> I believe that CH-weak reduction is may be related to calculi with explicit
> substitutions.
> CH-weak reduction is "more confluent" than standard reduction, as reducing
> (lam x. A) B preserves the property that B is in reducible position. (This
> is not true of standard weak reduction, consider the case where A is (lam y
> . C)). This property that head reduction preserves reducibility of their
> subterms also holds for explicit substitution calculi.
> 
> On Sun, Feb 25, 2018 at 12:06 PM, Filippo Sestini <[email protected]
>> wrote:
> 
>> [ 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
>> [email protected]
>> (+39) 333 6757668
>> 
>>