Re: [isabelle] Bound variables in Code_Evaluation.term



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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