Functional - mathementical/formal methods

Author

mathementical/formal methods - Feedback

news@absamail.co.za

2007-03-25, 7:03 pm

I originated 2 threads on this topic, which grew to over 100 responses
and threw up a few buzz-phrases which I was able to google on.
Currently I don't have a good threading newsreader; and it seems that
serious discussions have moved to blogs -- apparently due to spam.
Would I get a better response from eg.
http://lambda-the-ultimate.org ?

So far the best fetched material, suggests that what I'm 'looking for'
does exists. Eg.
http://www.mactech.com/articles/mactech/Vol.07/07.05/
LambdaCalculus/
> "A Calculus for the Algebraic-like Manipulation of Computer Code"

Some of his [optimistic for me] statements are:
> Wouldn't it be nice to be able to manipulate computer code in the same
> sort of clean mathematical way that one does algebra? Usually computer
> code is too ad hoc to allow much of that, but what if we had a super
> clean model that we could work with? Even if such a model wasn't
> practical, it would certainly still be interesting, and what could be found
> out from it might be mappable back into computer languages which
> don't have as neat a set of "algebraic-like" properties.
> ...
> This article will introduce l-calculus and combinators, and show some
> similarity between l-calculus and the programming language LISP. An
> attempt will then be made to use l-calculus as a programming language
> in its own right to code a popular function in an effort to show the
> clean, algebraic-like properties of l-calculus and to consider (in a
> small way) if l-calculus might serve as a "light unto the footsteps"
> to guide the way to computing without gratuitous complexity.

Perhaps what I'm hoping for is not quiet what he
[André van Meulebrouck] is explaining.

His 1'000 line article handles [nicely] sequentially:
Intro to l-calculus, LISP 10, Currying, Free Variables and Higher-Order
Functions, Intro to Combinators, Programming with Combinators,
Church Numerals, Arithmetic Functions, The Y Combinator, Aftermath;
which are each individually understandable sections.

But I can't see how they form an inference chain to the hoped-for
conclusion.

Perhaps my extreme hatred of top-posters is caused by an unnatural
inability to 'connect/handle mis-sequenced information' ?
IMO the correct way to explain a complex topic is by backward chaining.
Ie. top-down decomposition: the same way as programming is best done.
Eg. we want to acheive X,
which requires X1, X2...Xn,
which requires X11, X12....X21, X22...

Ie. the goal must be stated up front and be kept in sight and it must
be always clear that/how each step will lead to the goal.
Which is the principle of "Hello world". Ie. start with a minimal but
complete [up to the conclusion] explanation/statement. And proceed
by successive refinement.

His article seems to be suggesting the conclusions which I hope for,
namely eg. :
* any algorithm can be expressed in some minimum/cannonical syntax,
* which can be transformed to equivalent syntax[s]: S;
* which satisfy 'mathemetical' rule-set M;
* and allows manipulations P;
* which can arrive at conclusions C, for the original algorithm/code.

Where would I find on-line collaborators to help me build a 'complete'
if minimalist understanding of the available theory for this topic ?

Thanks for any info.

== Chris Glur.

Paul E. Black

2007-03-26, 7:04 pm

On Sunday 25 March 2007 12:31, news@absamail.co.za wrote:
> So far the best fetched material, suggests that what I'm 'looking for'
> does exists. Eg.
> http://www.mactech.com/articles/mactech/Vol.07/07.05/
> LambdaCalculus/
>
> ...
>
> But I can't see how they form an inference chain to the hoped-for
> conclusion.
>
> ...
>
> Where would I find on-line collaborators to help me build a 'complete'
> if minimalist understanding of the available theory for this topic ?

Lambda calculus, combinators, et. al. are great for proving
theoretical foundations, but they will never be practical. That is,
major programming languages will never look like that.

For a production language which is formally provable, I suggest
something like SPARK Ada
http://www.praxis-his.com/sparkada/

-paul-
--
Paul E. Black (p.black@acm.org)

Thomas Hafner

2007-03-27, 7:08 pm

"Paul E. Black" <p.black@acm.org> wrote/schrieb <eu8rpq02645@news3.newsguy.com>:

> Lambda calculus, combinators, et. al. are great for proving
> theoretical foundations, but they will never be practical.

But Lisp languages are practical, for instance. Emacs is practical,
because it can be highly configured (by a Lisp language).

Regards
Thomas

Apesto

2007-04-21, 8:26 am

http://Halle-Berry-anal-action.org/...hp?movie=148803

Sponsored Links