[mercury-users] Questions about declarative semantics of Mercury programs

[Fergus Henderson]

On 07-Jan-2003, Peter Moulder <pmoulder at mail.csse.monash.edu.au> wrote:
> One hoped-for advantage of Mercury is ease of reasoning.  In
> particular, one would expect to be able to mechanically transform the
> source of "pure" & valid (compileable) mercury programs into
> statements in predicate calculus, and apply the rules of predicate
> calculus to reason about Mercury "predicates" (ignoring
> completeness/termination properties).

Yes.

> The language reference manual has this to say about declarative
> semantics:
> 
> # For each legal Mercury program, there is an associated predicate
> # calculus theory whose language is specified by the type declarations
> # in the program and whose axioms are the completion of the clauses
> # for all predicates in the program, plus the usual equality axioms
> # extended with the completion of the equations for all functions in
> # the program, plus axioms corresponding to the mode-determinism
> # assertions (*note Determinism::), plus axioms specifying the
> # semantics of library predicates and functions.  The declarative
> # semantics of a legal Mercury program is specified by this theory.
...
> I'd like to make this more formal/detailed.

Good idea.

> For example, I'm not sure whether function application (in particular
> for semidet functions) can be reproduced unchanged when converting to
> logic statements or whether they must be transformed into predicate
> calls at the same time as transforming various other bits of syntactic
> sugar (syntactic sugar cubes?).

The intent was that they could be reproduced unchanged.
I'm not sure if this actually works, though.

> (Subtypes, once decided on, may pose similar questions: e.g. whether
> or not one can reasonably avoid transforming into base type with mode
> modifications in order to reason about a program.  Presumably it is
> intended that the answer be `yes'; in which case the question of how
> the Mercury->logic transformation rules should be modified will
> arise.)

The standard target for such a transformation -- polymorphic
many-sorted (PMS) predicate calculus -- does not support sub-types.  So yes,
you will need to replace sub-types with their base type when converting
to PMS predicate calculus.

(Alternatively, I suppose it might be possible to use a different typed
logic that included a notion of sub-types, rather than PMS predicate calculus.
But I haven't really thought too much about that.)

> Personally, I'm also unsure what "whose language is specified by the
> type declarations in the program" means.  If a program has two types
> 
>   :- module hello.
>   ...
>   :- type fruit ---> apple ; orange ; lemon.
>   :- type colour ---> red ; orange ; yellow.
> 
> then what is the language of the theory?

The language of the theory is the language which has
a type "hello__fruit",
a constant "hello__fruit/0__apple" of type "hello__fruit",
a constant "hello__fruit/0__orange" of type "hello__fruit",
a constant "hello__fruit/0__lemon" of type "hello__fruit",
a type "hello__colour",
a constant "hello__colour/0__red" of type "hello__colour",
a constant "hello__colour/0__orange" of type "hello__colour",
and a constant "hello__colour/0__yellow" of type "hello__colour".

> I'd also appreciate seeing
> how
> 
>    std_util__type_of(orange `with_type` fruit)
>      \= std_util__type_of(orange `with_type` colour)
> 
> should be handled.

When translated to (PMS) predicate calculus, that goal would be

    some [X : 'hello__fruit', Y : 'hello__colour'] (
    	X = 'hello__fruit/0__orange',
    	Y = 'hello__colour/0__orange',
        std_util__type_of(X) \= std_util__type_of(Y)
    )

which is equivalent to just

    'std_util__type_of'('hello__fruit/0__orange') \=
    'std_util__type_of'('hello__colour/0__orange')

Why did I introduce the variables X and Y here?
Although they are not needed in this example,
there are other examples in which they cannot be
so easily eliminated.  A more interesting case is

	:- pred main(io__state, io__state).
	main(S0, S) :-
		io__print(std_util__type_of(X `with_type` fruit), S0, S).

which when translated to (PMS) predicate calculus would become

	main(S0, S) <=>
		some [X : 'hello__fruit']
		'io__print'('std_util__type_of'(X), S0, S).

This could be further translated into single-sorted predicate calculus as

	main(S0, S) <=>
		(has_type(S0, 'io__state') /\
		 has_type(S, 'io__state') /\
		 (some [X] (has_type(X, 'hello__fruit') =>
			'io__print'('std_util__type_of'(X), S0, S)))).

> Another thing is induction.  Given:
> 
>   :- type ordinal ---> first ; succ(ordinal).
> 
> is it true to say
> 
>   all[P] (  (
>                 P(first),
>                 all[X] (P(X) => P(succ(X)))
>             )
>             => all[X] P(X)
>          )
> 
> (apart from some clutter specifying the types of P and X) ?

Whether or not it is "true" might depend on which model of the theory you use.
I guess you want to know whether or not it is "valid", i.e. true in all models.
I don't know the answer to that.
However, if you want such an axiom, you can certainly add it.

Perhaps Mercury's standard declarative semantics should also include
such an axiom.

> (A consequence of this would be that terms are never "rational"/cyclical;

> Indeed, what are "the usual equality axioms"?

The original intent was the ones specified by Clark.
I think the following reference has them:

	K. L. Clark. Negation as failure. In H. Gallaire and J. Minker,
	editors, Logic and Databases, pages 293--322, Toulouse, France,
	1978. Plenum Press.

Unfortunately this is a bit too old to google for.

I think Clark's axioms include some occurs-check axioms which
ensure that terms are never cyclical.  But I don't know
if these axioms imply the induction law that you mentioned above.

So, the original intent was to use Clark's equality axioms,
and I think Clark's equality axioms imply that terms are never
acyclic.  However,  I don't think we fully understood the consequences
of this at the time.  I think the issue of whether or not Mercury's semantics
should include axioms which ensure that terms are acyclic needs
to be given more consideration, especially in the light of the
"lazy" and "store" modules, and interfacing with other languages.

Also, we may need some additional axioms (e.g. see below).

> Taking ordinal as an
> example, I think I've been using the above induction rule and the
> following:
> 
>   all[X]  (first \= succ(X)).
>   all[X, Y]  ( succ(X) \= succ(Y) ; X = Y ).
>   all[X]  (  not has_type(X, ordinal)
>            ; X = first
>            ; some[Y] (X = succ(Y), has_type(Y, ordinal)) ).

I certainly think that these should be included in "the usual equality
axioms".  The first two are consequences of Clark's axioms, I think,
but the last one -- which expresses the "exhaustiveness" of the
different functors in a type definition -- won't correspond to anything
in Clark's axioms, I'm pretty sure, since Clark was working in an
untyped (single-sorted) setting.  We should add those.

> The way I usually handle type restrictions is to transfrom
> `some[X] (EXPR(X))' where X has type foo to
> `some[X] (has_type(X, foo), (EXPR(X)))'.  (Accordingly,
> `all[X] (EXPR(X))' becomes `all[X] (not has_type(X, foo) ; (EXPR(X)))'.)
> This allows use of the last of those rules and the above induction rule.
> (The "clutter" I referred to above for the induction rule, I'd express
> in terms of `not has_type' disjuncts.)  Is there a better way, as far
> as formalisation goes?

That is the right way to transform things if you want to go to
single-sorted predicate calculus.  Another alternative is to stop
at many-sorted predicate calculus, with `some [X : foo] (EXPR(X))'.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------