Failure-handling as fundamental

[Francois-Rene Rideau]

Hi Iepos! Nice to hear from you!

On Sat, Feb 02, 2002 at 02:52:06AM -0700, Brent L Kerby wrote:
> The central idea I realized was that failures (or exceptions),
> and constructs for handling failures, naturally form a part
> in the very foundation of mathematics and computation.  [...]
>
>   A "true" program is one which terminates without failure.
>   A "false" program is one which fails.
>
> Fare has hinted at this idea before, long ago, in his paper on Reflection, I
> believe.
>
Actually, it was the central idea of my Master's Thesis on a logic system
best suited for integration in a pure applicative untyped programming
language (a Scheme subset). In my paper "Reflection, Non-determinism and
the Lambda-calculus", I showed how to build some kind of reflective
system based on the idea.

As for using this idea in programming languages, logic programming language
kind of do it with Prolog and its successors like Oz or Mercury.

A language with a much more imperative feeling that does it is Icon,
(by the author of SNOBOL). It's a language you should study, if you're
interested in this approach (and certainly I should study it, too).
Hum. Maybe a language to add to the TOP list of languages to consider,
in Review/Languages.html

> [...] this system [...] reconciles the paradoxes; [...]
> We'll find that when paradoxical statements are translated
> into this formalism, they simply become non-terminating programs;
> thus they are neither true nor false, and we can see why and be satisfied.
>
That was also the argument I used in my Master's Thesis.
In other words, we have an intuitionnistic logic,
rather than a classical logic where all programs either terminate
or have their negation terminate (can be proved to fail in finite time).

> "undo" is literally the Church number for "-1"
I've seen pages of people studying lambda-calculi with such a number,
but I admit I don't know much about them.

> So what does this have to do with failures? [...]
> Now, here is something interesting ... the very operator of
> equality can be constructed neatly from "undo" as
>    [dup] undo
My Master's thesis also used such trick to show that equality of functional
objects was definable in the formalism (but of course didn't have
to terminate). Actually, I defined undo from equality rather than the other
way around. Hence, yielding logic programming from within a
non-deterministic functional programming language with reasoning.
Equality could either be a non-computable external axiom, or it could be
computationally defined as proof of equality within a reflective set
of axioms, the completeness of which is self-fulfilling
(was a nice result I realized while writing the rndlc paper,
after my Master's Thesis).

>   or ==  A\ B\  [[B] not [A] not] not
Actually, if your or is to yield usable values, rather than just termination,
you'll find that it's 
	B A or == [[B] not [A] not and] not
also, or is often easier to implement than and.
Finally, in intuitionnistic logic,
these boolean laws might or might not hold,
with or A B yielding less values than [[B] not [A] not and] not.

> Meanwhile, I think I'll try to make a little prototype implementation
> of this kind of system (a Joy-like one, but with failures and
> failure-handling, and also with a style of variables,
> but of course not with "undo").
I admit my system was never implemented. Beware, because
* implementing the full logic means a combinatorial explosion,
 as the system looks for all possible proofs of evaluated logical constructs
* thus you must (begin with) only implementing a computational subset
 of the system
* only after you have done so can you begin bootstrapping the full logic
* even then, you'll actually be interested in manipulating logical terms
 without really evaluating them, until the last moment, when you evaluate
 them within a given strategy.
* having documented the logic system says nothing of the proof language
 and the strategy language, which are actually most important.

Good luck,

[ François-René ÐVB Rideau | Reflection&Cybernethics | http://fare.tunes.org ]
[  TUNES project for a Free Reflective Computing System  | http://tunes.org  ]
For every complex problem, there is a solution that is simple, neat, and wrong.
		-- H. L. Mencken