[Agda] Type-checker evaluator performance

[Peter Selinger]

Dear Nils,

thanks for these references. All of them are interesting. But as far
as I can tell, none of these papers is exactly what is needed to
implement efficient call-by-name reduction.

The Crégut papers are about changing Krivine's machine to make it
produce normal forms (as opposed to head normal forms), but it does
not address the non-lazyness of Krivine's machine, i.e., the lack of
sharing and the ensuing repeated evaluation of an expression.

The Grégoire-Leroy paper is about the same thing, but for
call-by-value, so it is also not lazy.

The Benaissa-et-al paper is about a syntax for explicit
substitutions. I didn't read it carefully enough to be completely sure
whether the resulting sytem implements any kind of sharing, but I
rather get the impression that this is not the case. The example, the
reduction rule (in Figure 5) (a b)[c/] -> a[c/] b[c/] seems to
indicate that the (potentially large) term c is duplicated before it
is evaluated.

-- Peter

Nils Anders Danielsson wrote:
> 
> On 2016-02-02 08:31, Jon Sterling wrote:
> > I hope this isn't off-topic, but what's the state of the art for this?
> > Krivine machines?
> 
> I don't know, I know very little about this topic.
> 
> Randy Pollack once informed me that LEGO uses the U-machine (due to
> Pierre Lescanne) for strong reduction:
> 
>    λν, a calculus of explicit substitutions which preserves strong
>    normalisation
>    Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne and Jocelyne
>    Rouyer-Degli
>    http://doi.org/10.1017/S0956796800001945
> 
> He also mentioned a machine due to Pierre Crégut:
> 
>    An abstract machine for Lambda-terms normalization
>    Pierre Crégut
>    http://doi.org/10.1145/91556.91681
> 
> An extended version of the paper above:
> 
>    Strongly reducing variants of the Krivine abstract machine
>    Pierre Crégut
>    http://doi.org/10.1007/s10990-007-9015-z
> 
> Is this the kind of thing you have in mind? Or maybe the following
> machine?
> 
>    A Compiled Implementation of Strong Reduction
>    Benjamin Grégoire and Xavier Leroy
>    http://doi.org/10.1145/583852.581501
> 
> -- 
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>