[mercury-users] Pred defns

[Ralph Becket]

Fergus Henderson wrote on 5 Apr:
> On 02-Apr-1998, Ralph Becket <rwab1 at cam.sri.com> wrote:
> ...
> On that point, I agree that adding quantifiers would not be a good solution.
> I was not proposing that, I was just using them to explain why upper
> case accumulator names don't work.  My preference would be to use
> lower case accumulator names.

Okay - I'm still not 100% convinced, but it's a minor niggle!

> > I'm going to go out on a limb here and may get (justifiably) shot down
> > in flames, but... why don't we bite the bullet and accept that bits of
> > source code written in this style will not be syntactically identical
> > with its FOL denotation?
> 
> This is a good question.
> 
> My answer is to say that ensuring "Clean Denotational Semantics of
> Source Code" is one of the foremost goals of Mercury.  This is one
> of the few things that really distinguishes Mercury from hundreds of
> other languages out there.  One of the key features of Mercury is
> that it takes the ideal of PROgramming in LOGic and makes it a
> reality -- your program is indeed a set of statements in logic, and
> the implementation is guaranteed to be sound with respect to that
> logic.
>
> As soon as you depart from this direct programming-in-logic and
> instead use
> programming-in-something-that-can-be-translated-into-logic you have
> stepped off the One True Path onto a slippery slope.  Just a little
> way down the slope, guided by Paul Voda's paper "a logical
> reconstruction of a one-solution operator", you will find Trilogy's
> `once' operator; Prolog's cut is not far below.  Somewhere down at
> the bottom of the gully lies C++ ;-)

Yes, I can't argue with the intention, but I'm not totally sure it's
realizable - and you do use DCGs in quite a bit of Mercury code!

This whole debate is about how to help programmers by abbreviating a
common idiom (accumulator threading) in as clean a way as possible and
nobody's yet suggested anything that satisfies the Program as (just)
Logic criterion.  That's why I suggest keeping the transformation very
simple so that there's only the tiniest deviation from the True Path -
once/1 and cut have a non-obvious effect on semantics and are not just
a jump to the left, they're the whole Time Warp!

It occurs to me that the implicit threading idea relies upon the order
in which goals occur in a clause as written by the programmer.  This
is exactly where the threading information comes from!

Cheers,

Ralph

-- 
Ralph Becket  |  rwab1 at cam.sri.com  |  http://www.cam.sri.com/people/becket.html