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.

Cheers,
Andreas

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
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?

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





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