[mercury-users] The Logic of Mercury

[David Glen JEFFERY]

On 08-Sep-1999, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> 
> append :: list(T) -> list(T) -> list(T) -> pred
> ',' :: pred -> pred -> pred
> 
> I have also tried (and failed) to construct a type system which avoids the
> -> pred all over the place.

> I believe the details have been worked out for Lambda Prolog (they use 'o'
> instead of 'pred'), though I haven't actually seen a full type system
> described and there might still be some problems.

There is a description in Chapter 9 of the `Types in Logic Programming' book
edited by Frank Pfenning. (Of course, your copy of the book has been sitting
on my desk for the last year or so, though ;-) ).

The typing rules, unsurprisingly, look just like those of a typed lambda
calculus.

BTW, the use of `o' to represent the predicate type goes all the way back
to Church's original formulation of the simple theory of types in 1940. 
Church's original type system is seems very similar to Lambda Prolog's.


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) | If your thesis is utterly vacuous
PhD student,                    | Use first-order predicate calculus.
Dept. of Comp. Sci. & Soft. Eng.|     With sufficient formality
The University of Melbourne     |     The sheerist banality
Australia                       | Will be hailed by the critics: "Miraculous!"
                                |     -- Anon.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------