Re: [isabelle] Bound variables in Code_Evaluation.term

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.


On 18/06/14 22:06, Florian Haftmann wrote:
Hi Andreas,

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

   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?

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,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.