Lambda-Calculus
RE01 Rice Brian T. EM2
BRice@vinson.navy.mil
Fri, 16 Oct 1998 20:31:55 -0700
>> I don't think I'm "sold" to lambda-calculus (as I've read in another
>>message
>> in this list). Perhaps there are simpler concepts that subsume
>> lambda-calculus and give better insight into programming languages;
>> if there are, I'll be glad to learn about them. I haven't seen them yet,
>> and lambda-calculus is so simple that I'd be surprised if/when I meet them.
>
>New things are always suprising. Almost always; sometimes their
>unsuprisingness is
>the thing that suprises me.
>
>Take a look at Abstract State Machines (Evolving Algebras) for an example
>right in
>your department (proof of correctness, translation from concept to code). I
>for
>one consider them to be more useful than the lambda calculus, in that they
>adjust
>to how the machine works as well as how the algorithm works (and that
>adjustment
>can be tuned by the evaluator).
Thanks for the responses. I agree with your ideas. I guess I should
explain that I'm currently trying to condense all the ideas that have
been floating around my head for years into a workable prototype (the
kernel that I've spoken of). So, please excuse all my ramblings and
soap-box speeches in exchange for my offering of the prototype system to
result from these conversations (hopefully in a few months). I've got
my head deeply buried into recent mathematics papers, and so I feel the
need to bounce ideas off of others, even though I may not agree with
them (this applies to several things I have said) in order to force
myself to find a solution.
I have to admit that lambda-calculus, through currying and advanced type
information, is indeed complete in supporting the kind of system I am
looking for, but not in a first-order way. The state-machine algebra
seems to be right along the path that I'm looking for, having a more
intuitive approach to describing abstract objects for interaction with
the system. Let's say my complete solution would be to include all
algebras for inclusion into the language of the system I'd like to
build, with a complete set of transformations available allowing the
translation of, say, a state-machine diagram into a lambda-form (due to
model theory, possibly). The transformations, I believe, should be
available from an information theory based on arrow-diagrams, for
instance, or some other graph theory derivative. The language for the
transformations would, of course, be available to translate to or from.
Does this sound like a good approach?