11
$\begingroup$

The following term (using bruijn-indexes):

BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0)))))))))

When applied to a church number N evaluates to normal form quickly in several existing evaluators, including naive ones. Yet, if you encode that term to interaction nets and evaluate it using Lamping's Abstract Algorithm, it takes an exponential numbers of beta-reductions in relation to N. On Optlam, specifically:

N   interactions(betas)     (BADTERM N)
1   129(72)                 λλλ(1 (2 (2 (2 (2 (2 (2 (2 0))))))))
2   437(205)                λλλ(2 (1 (2 (2 (2 (2 (2 (2 0))))))))
3   976(510)                λλλ(1 (1 (2 (2 (2 (2 (2 (2 0))))))))
4   1836(1080)              λλλ(2 (2 (1 (2 (2 (2 (2 (2 0))))))))
5   3448(2241)              λλλ(1 (2 (1 (2 (2 (2 (2 (2 0))))))))
6   6355(4537)              λλλ(2 (1 (1 (2 (2 (2 (2 (2 0))))))))
7   11888(9181)             λλλ(1 (1 (1 (2 (2 (2 (2 (2 0))))))))
8   22590(18388)            λλλ(2 (2 (2 (1 (2 (2 (2 (2 0))))))))
9   43833(36830)            λλλ(1 (2 (2 (1 (2 (2 (2 (2 0))))))))
10  85799(73666)            λλλ(2 (1 (2 (1 (2 (2 (2 (2 0))))))))
11  169287(147420)          λλλ(1 (1 (2 (1 (2 (2 (2 (2 0))))))))
12  335692(294885)          λλλ(2 (2 (1 (1 (2 (2 (2 (2 0))))))))
13  668091(589821)          λλλ(1 (2 (1 (1 (2 (2 (2 (2 0))))))))
14  1332241(1179619)        λλλ(2 (1 (1 (1 (2 (2 (2 (2 0))))))))
15  2659977(2359329)        λλλ(1 (1 (1 (1 (2 (2 (2 (2 0))))))))

On similar evaluators such as BOHM, it takes much less beta steps, but more interactions. If optimal evaluators are optimal, how can they evaluate terms asymptotically slower than existing evaluators?

This link has an explanation about the origin of the term, as well as an implementation of the same function that behaves the opposite, almost bizarrely so: it should run in exponential time - it does run in exponential time in most evaluators - yet, optimal evaluators normalize it in linear time!

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

Efficiency of optlam

I have not studied the details of BADTERM nor of the implementation of optlam evaluator, but I find quite strange that optlam performs a number of ß-interactions drastically different than another optimal evaluator like BOHM. Such a number must be, by definition, basically the same on a given term. Are you sure of the correctness of optlam's core?

Efficiency of optimal evaluators

Recall that the notion of optimality of these evaluators is more properly known as Lévy-optimality, and it is not the naive one, since a strategy of reduction performing the minimum number of ß-steps is not computable. What is minimised, then, is the number of parallel ß-reduction steps performed on a whole family of redex, that is roughly the set obtained by the symmetric and transitive closure of the relation which binds two redexes when one is copied from the other. It should in general not surprise to see discrepancies between the number of ß-steps and the rest of duplication-steps, since we know that most of the normalisation load could be transferred from the former to the latter, as shown by Asperti, Coppola and Martini [1].

It should not surprise us either to see that total number of interactions needed to normalise an term with an optimal evaluator is that lower than with an ordinary one, since previous empirical observation already showed notable performance improvements. In spite of this, such a huge complexity jump, from exponential to linear time, is perhaps the very first of its kind being being discovered, though. (I will check this.)

On the other hand, the theoretical results about the efficiency of optimal reduction (which is your big question), are still few and not yet general, since they are limited to EAL-typed proof-nets (which is basically the same restriction of optmal evaluator, if I correctly understand), but all are mildly positive, since in the worst case the complexity of sharing reduction is bounded by the ordinary one by a constant factor [2,3].

References

  1. A. Asperti, P. Coppola, and S. Martini, (Optimal) Duplication is not elementary recursive, Information and Computation, vol. 193, 2004.
  2. P. Baillot, P. Coppola, and U. Dal Lago, Light logics and optimal reduction: Completeness and complexity, Information and Computation, vol. 209, no. 2, pp. 118–142, 2011.
  3. S. Guerrini, T. Leventis, and M. Solieri, Deep into optimality – complexity and correctness of sharing implementation of bounded logics, DICE 2012, Tallin, Estonia, 2012.
Improve this answer
$\endgroup$
8
  • $\begingroup$ Such a number must be, by definition, basically the same on a given term so I thought. That surprised me since Optlam gives the same number of betas as BOHM in many cases I tested. In some cases it gives less, though, due to its call-by-need strategy. Someone told me reduction without the oracle isn't actually optimal and now I don't know anymore. All in all, I'm deeply confused. But no, there is definitely no proof Optlam operates correctly at all. I'm thinking about the rest of your comment - thank you. $\endgroup$
    – MaiaVictor
    Oct 21, 2015 at 15:09
  • $\begingroup$ Moreover, I've actually found many different terms that behave just like Badterm. I'm studying the issue further so I can find simpler terms that replicate it. $\endgroup$
    – MaiaVictor
    Oct 21, 2015 at 15:12
  • $\begingroup$ A sort of parallel call-by-need strategy is standard for optimal evaluators, including BOHM, since it is necessary for Lévy-optimality itself. The oracle is not strictly necessary to optimal-reduce any λ-terms: stratified terms, such as EAL-typed ones, do not need it. $\endgroup$
    – Marco Solieri
    Oct 21, 2015 at 15:54
  • $\begingroup$ Oh, my bad, then. Anyway, just to make sure I understand it, when you account for duplication (not just betas), there can be terms that are asymptotically slower to reduce on optimal evaluators, even on the EAL-typed case? In that case I'd wonder why it is meaningful to count beta steps only and if there is really any benefit in using interaction nets for the purpose of λ-calculus reduction... $\endgroup$
    – MaiaVictor
    Oct 21, 2015 at 16:01
  • 1
    $\begingroup$ Aha! So there are non EAL typeable terms that can be reduced without the oracle? I assumed if Optlam reduced it, it was EAL-typeable (since I don't have an EAL type inferencer). If that isn't the case, then everything makes sense now. Since the subset of EAL-typeable terms has enough power to express any poly-time algorithm like sorting, I guess it would me wise to specifically attempt to design EAL-typeable terms. I wonder how it could be done in practice, though. Thank you so much. $\endgroup$
    – MaiaVictor
    Oct 21, 2015 at 16:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.