Email Gateway (Aug 22 2022 at 15:34): Email Gateway (Aug 22 2022 at 15:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I've read in the paper on Isabelle's normalisation-by-evaluation mechanism (Aehlig,
Haftmann, Nipkow, JFP 22(1), 2010) that it is supposed to delay the evaluation in the
branches of case expressions (Section 5.2) until it is clear which case to evaluate.
Unfortunately, this seems to be broken in some cases. Here's a contrived example:
definition silly :: "nat => nat" where "silly _ = 0"
lemma [code]: "silly n = id (case n of 0 => silly (Suc 0) | Suc n => silly n)" sorry
value [nbe] "silly n" (* does not terminate *)
As the argument to silly is a variable, I would have expected that this returns "silly n"
or maybe "case n of 0 => silly (Suc n) | Suc n => silly n", but the call to value loops.
Interestingly, when I drop the "id" in the above code equation, then NBE does terminate
with the expected result. Is this intended? Can I somehow enforce that the branches of a
case are evaluated only after it is clear which branch to take?
Best,
Andreas
Email Gateway (Aug 22 2022 at 15:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
you can inspect code generated by NBE using
declare [[nbe_trace]]
Note that this is extremely arcane to study, though.
Concerning your particular observation: case matches are treated
differently a) on top level of rhs b) inside a nested term expression.
a) is implemented the same way as pattern match failure on LHS: a failed
pattern match advances to the next code equation. Using the same
operational semantics in case b) would require a more sophisticated code
generation, either involving exceptions or some kind of option monad,
which we have been reluctant to undertake; instead, the case combinator
is left as it is, but the other terms of the case expression are normalized.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 15:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
Thanks for the quick answer. Looking at the code, I can see the difference in treatment.
I had hoped that there was some clever trick to delay the normalisation of the branches in
the code and that I might be able to use the same trick to stop NBE from expanding
corecursive definitions for ever. But as is, it seems impossible to get lazy evaluation
with NBE. :-(
Best,
Andreas
Last updated: Apr 25 2024 at 04:18 UTC