oleg at pobox.com oleg at pobox.com
Tue Jul 19 00:56:17 EDT 2005

```Regarding the law of mif (aka ifte, aka soft-cut, aka logical
conditional)

mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e)

You're right of course: mode matters for the predicates that involve
negation, such as mif. However, I believe that the mode is orthogonal
to the discussion of the mif law. The following is a better
example. Again we will be using Prolog (with the built-in
soft-cut). This time, we eschew any variable binding within our
conditionals, in fact, any variables at all. Truth and failure is all
we need.

We chose c === (true; true), t' === e' === fail,
t === e === true. Thus,

mif (mif c t' e') t e
translates to {X =1 is there so that Prolog will print something}

X = 1, (((true; true) *-> fail; fail) *-> true; true).

mif c (\x -> mif (t' x) t e) (mif e' t e)
translates to

X = 1, ((true; true) *-> (fail *-> true; true) ; (fail *-> true; true)).

and returns two answers, 1 and 1.

Indeed, using the semantics of the soft cut, we find that the first
translation reduces to
X = 1, true.
whereas the second one reduces to
X = 1, (true; true)

```