[m-users.] comprehension question

[Volker Wysk]

Am Freitag, den 25.10.2019, 19:50 +1100 schrieb Mark Brown:
> Hi Volker,
> 
> On Fri, Oct 25, 2019 at 6:21 PM Volker Wysk <post at volker-wysk.de>
> wrote:
> > Hi!
> > 
> > I have a question. I don't understand, why this doesn't work. This
> > is
> > the backwards direction of error() from the posix library:
> > 
> > :- pred error1(int, posix.error).
> > :- mode error1(out, in) is det.
> > %:- mode error1(in, out) is det.
> > 
> > error1(Num, Res) :-   ((  Num = 0,    Err = e2BIG
> >     ;   Num = 1,    Err = eACCES
> >     ;   Num = 2,    Err = eAGAIN
> >     ;   Num = 3,    Err = eBADF
> > (...)
> >     ;   Num = 39,   Err = eSPIPE
> >     ;   Num = 40,   Err = eSRCH
> >     ;   Num = 41,   Err = eTIMEDOUT
> >     ;   Num = 42,   Err = eXDEV
> >     ) ->
> >         Res = Err
> >     ;
> >         Res = unknown(Num, "unknown errno")
> >     ).
> > 
> > I get this message from the compiler:
> > 
> > strerror.m:072: In clause for `error1(out, in)':
> > strerror.m:072:   scope error: attempt to bind a non-local variable
> > inside the
> > strerror.m:072:   condition of an if-then-else.
> > strerror.m:072:   Variable `Num' has instantiatedness `free',
> > strerror.m:072:   expected instantiatedness was `unique(0)'.
> > strerror.m:072:   The condition of an if-then-else is only allowed
> > to
> > bind
> > strerror.m:072:   variables which are local to the condition or
> > which
> > occur
> > strerror.m:072:   only in the condition and the `then' part.
> > 
> > 
> > Shouldn't this work in both directions? I think it's logical...?
> 
> The relation is injective but not bijective, so it would not actually
> be logical to declare the reverse mode det.
> 
> It would be logical to declare the reverse mode semidet, in the sense
> that it would be consistent with the declarative semantics, but that
> doesn't mean it should work operationally. Mercury uses
> negation-as-failure to implement if-then-elses and this is unsound if
> you bind variables in the way the error message describes; that's why
> it is disallowed.

Does that mean that

  ( if p
    then q
    else r )

is operationally equivalent to

  ( p,
    q
  ; not(p), 
    r
  )

?

I don't understand the soundness part. How should the predicate to be
done?

Respectfully,
Volker