Hi,
I have an inductive datatype Exp with pointers (nums) at some leaves.
I have a function, foo, that generates an Exp, and an environment (:num |->
Exp).
The idea is that the "real" Exp is the one you get by substituting the
things in the environment for the corresponding numbers.
But let's suppose I don't want to actually use the datatype that would let
me create the "real" Exp: I want the pointers there because it simplifies
other things.
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
- 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.
There seem to be obvious design patterns here.
Are there reasoning patterns to accompany them?
How might I define my types and functions to make reasoning easier?
Is there any binding here? I don't think so (and hope not!). There is
reference, though.
Let me know if anything is too vague.
I look forward to hearing from you.
Cheers,
Ramana
------------------------------------------------------------------------------
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
