--- Kevin Toppenberg <[EMAIL PROTECTED]> wrote:
> > Greg, I'm glad we have people like you to think about these > things...., because right now this is over my head! > > :-) > > Kevin Basically, it's about generalizing relations withing the context of type theory (which caught my attention because it's something I've been thinking about, even if I haven't talked about it much on Hardhats). It also has some interesting criticisms of the relational model. Domain theory is kind of like a structured set theory that allows you to "solve" equations representing recursive relationships. I put "solve" in quotes, because the solutions turn out to be fixed points of an operator that can be realized through a series of approximations at the domain level, and that sequence of approximations is essentially the unfolding of a recursive definition into iterative form. I know I'm only offering hints here, but a domain is basically a special kind of partially ordered set where the partial order is represents computational approximation. I don't know if anyone read my little post about "counting to infinity", but it provides an interesting hint here. The following Haskell program fix f = f (fix f) g f n = n : f n h f = 1 : map (+1) f provides a recursive definition of the infinite list [1, 2, 3 ..] as the fixed point of the function that operates on this list by adding 1 to each element (to obtain [2, 3, 4 ..] and then sticking a 1 at the head of the list (to obtain [1, 2, 3 ..]). This is one method of expressing recursion, but the point is that it illustrates how the fixpoint operator (also called the paradoxical operator!) can be used to define recursive *structures*, thus giving you a mathematical framework for introducing such things as trees and lists as data types. But there's more to the story, too. This framework makes it easy to translate recursive definitions into a framework known as lambda calculus (introduced by Alonzo Church), and lambda expressions can be mechanically evaluated. I've spoken to a few people off-line about the possibility of a "Functional MUMPS" or "Functional Fileman". The question is whether very large shared data structures (like globals) can *efficiently* be dealt with in the context of lambda calculus. If the answer turns out to be yes, that opens up the door to a referentially transparent (no indirection, no dangling pointers and more) method of reasoning about globals and programs, even the possibility of proving correctness of VistA code. So, if it seems like I've fallen off the map a bit, well, perhaps the above examples will give some hints as to the nature of my little research project. === Gregory Woodhouse <[EMAIL PROTECTED]> "Interaction is the mind-body problem of computing." --Philip Wadler ------------------------------------------------------- This SF.Net email is sponsored by the JBoss Inc. Get Certified Today Register for a JBoss Training Course. Free Certification Exam for All Training Attendees Through End of 2005. For more info visit: http://ads.osdn.com/?ad_id=7628&alloc_id=16845&op=click _______________________________________________ Hardhats-members mailing list Hardhats-members@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hardhats-members
