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).
and returns one answer, 1.
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)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
