[mercury-users] Pred defns
rwab1 at cam.sri.com
Mon Apr 6 18:49:12 AEST 1998
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
> 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!
Ralph Becket | rwab1 at cam.sri.com | http://www.cam.sri.com/people/becket.html
More information about the users