Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bound variables in Code_Evaluation.term

Email Gateway (Aug 19 2022 at 14:35):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

the classical code evaluation (code_evaluation.ML and particularly
HOLogic.reflect_term) do not cover variables at all. This is an
extensions of quickcheck narrowing. You might start your investigation
there (grep -rIFn Code_Evaluation.Free .).

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 14:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,

Thanks for the hint to quickcheck narrowing. I now see that Code_Evaluation.Free is only
used to represent uninstantiated terms in counter examples. Abstractions only occur in
quickcheck exhaustive in the special case of dummy abstractions. So there currently is no
need to think about bound variables.

Cheers,
Andreas

Email Gateway (Aug 19 2022 at 14:46):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi,

I am trying to understand how the term representation in Code_Evaluation deals with variables.

The pseudo-constructors Const, App and Abs clearly model constants, application and
abstraction, but I am having difficulties with the purpose of Free. Is Free supposed to
model both bound and free variables?

For example, how is the Isabelle term "x (%x :: nat. x)" to be represented in
Code_Evaluation? Omitting the types, I came up with the following.

App (Free x ...) (Abs "x" ... (Free x ...))

However, it seems strange that the second occurrence of Free actually denotes a bound
variable. Is that intended?

Best,
Andreas

Last updated: Apr 20 2024 at 01:05 UTC