Replacing the CF axiom for app

[Koen Claessen]

For reference. An old e-mail explaining app and CF. /Koen

---------- Forwarded message ----------
From: Koen Claessen <ko...@chalmers.se>
Date: Fri, Aug 19, 2011 at 4:58 PM
Subject: Replacing the CF axiom for app
To: Simon Peyton Jones <sim...@microsoft.com>, Charles-Pierre Astolfi
<t-ch...@microsoft.com>

OK, here are my thoughts on CF and app.

We currently have an axiom:

 (old)  ![F] : ( CF(F) <=> (![X] : (CF(X) => CF(app(F,X)))) )

In other words, F is crash-free iff. applying it to anything
crash-free produces something crash-free.

We want to limit the application of this axiom using min. Here is how.

We first split the axiom into two axioms, going opposite directions.
Here is one direction:

 (old)  ![F,X] : ( CF(F) & CF(X) => CF(app(F,X)) )

In other words, applying a crash-free function to a crash-free
argument remains crash-free.

We only want to invoke the axiom if we are actually interested in
applying F to X:

 (new)  ![F,X] : ( CF(F) & CF(X) & min(app(F,X)) => CF(app(F,X)) )

Here is the other direction:

 (old)  ![F] : ( ~CF(F) => ?[X] : (CF(X) & ~CF(app(F,X))) )

(Remember that ? is existential quantification.) So, if F is not
crash-free, then there is a crash-free argument that makes F produce a
non-crash-free result.

Now, we want to invoke this axiom if we are interested in F (only!).
The invocation of the axiom should then make app(F,X) interesting too!
Here is how to say that:

 (new)  ![F] : ( ~CF(F) & min(F) => ?[X] : (CF(X) & ~CF(app(F,X)) &
min(app(F,X))) )

This seems silly though, because now *anything* which is asserted to
be not crash-free and interesting will be applied to an argument. (But
it is no worse than what we did before we had min!) It is not so bad
though: even though we will generate things like app(Nil,X) which do
not make any sense, there are no axioms that will be triggered by
this.

/Koen