On 12/10/12 05:09, Ramana Kumar wrote: > I have an inductive datatype Exp with pointers (nums) at some leaves. [...]
> I have written foo in monadic style over a state that includes the "next fresh > pointer" and the environment. > I don't care what the pointers are, and I'd be happy if they were all distinct > in any Exp (or even "globally", though that is impossible to define). > Reasoning about functions like foo would seem to require: > * defining a well-formedness on states, saying that anything in the > environment's domain is less than the "next fresh pointer" (and possibly > also for any pointers appearing in Exps in the range), and proving that > lots > of functions "maintain" well-formedness I think this one is pretty unavoidable. > * figuring out how to express the "core result" of foo, and seeding it with > any other initial pointer gives the same result modulo renaming all the > pointers > * proving that foo indeed produces Exps with distinct pointers throughout > (and > similarly for all foo-like functions) > But that sounds like a lot of tedious work. Welcome to interactive theorem-proving :-) Can you express the correctness of your constructions by talking about the result in terms of the value after having performed the substitution? Even if you do really want the type with pointers, you can prove something like ∀σ i v σ’. foo σ i = (v,σ’) ⇒ correct (apply_subst σ’ v) Michael ------------------------------------------------------------------------------ Don't let slow site performance ruin your business. Deploy New Relic APM Deploy New Relic app performance management and know exactly what is happening inside your Ruby, Python, PHP, Java, and .NET app Try New Relic at no cost today and get our sweet Data Nerd shirt too! http://p.sf.net/sfu/newrelic-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
