Dear Rasmus, Or you could use a logic based on a lambda-calculus with reflection:
http://www.comlab.ox.ac.uk/tom.melham/pub/Grundy-2006-RFL.pdf Best regards, Tom On 29 Sep 2010, at 18:10, Tjark Weber wrote: > 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). ------------------------------------------------------------------------------ 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
