Rasmus, On Wed, 2010-09-29 at 17:39 +0100, Rasmus Lerchedahl Petersen wrote: > I am trying to write a formula stating that one term is a substitution of > another, eg `is_sub P Q <=> P[z/x] = Q`, so that `is_sub (x+y) (z+y)` > should be true.
This is not possible: you cannot define a function that accesses the syntax of terms *in the logic*. Every function in the logic respects Leibniz's law, i.e., x = y implies f x = f y (where = is logical equality). Of course, you can easily define substitution etc. in the meta language (ML/OCaml). If you want to reason about the syntax of terms in the logic, you will need a deep embedding of your terms, i.e., you need to define a (recursive) data type (in the logic) that models the syntax. You will probably also want to define the semantics of terms (as a function on this data type). Hope this helps! Tjark ------------------------------------------------------------------------------ Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novell-sfdev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
