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

[Peter Moulder]

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).

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.
#
# Mercury implementations must be sound: the answers they compute must
# be true in every model of the theory.  Mercury implementations are
# not required to be complete: they may fail to compute an answer in
# finite time, or they may exhaust the resource limitations of the
# execution environment, even though an answer is provable in the
# theory.

I'd like to make this more formal/detailed.

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?).  (I've appended a program that
produces results I wouldn't expect, though I've never read how
quantifications involving partial functions behave in standard
mathematics.)

(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.)


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?  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.  (My solution would be qualifying symbols with both
module and "deep" type name, deep in the sense that list(foo) differs
from list(bar) so that [] `with_type` list(foo) behaves correctly.)

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) ?

(A consequence of this would be that terms are never "rational"/cyclical;
e.g. all[X] X \= succ(X).  Usually the mode checker prevents cycles,
though foreign code presents some opportunities.  The question is
reminiscent of Ralph(?)'s question to Fergus about the lazy module,
which uses foreign code to change the representation of `in'
arguments.)

Indeed, what are "the usual equality axioms"?  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)) ).

(Excuse the abuse with has_type's second argument.)


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?


Thanks for any light you can shed on these issues.

pjm.


% An example of where Mercury semantics give a result different from what
% I'd expect without transforming `\=' and transforming function calls to
% predicate calls.
% I'd expect B to equal C, and (perhaps with less certainty) I'd expect A
% to be "no".
:- module partial_fns.
:- interface.
:- use_module io.
:- pred main(io__state::di, io__state::uo) is det.
:- implementation.
:- use_module string.

:- type fruit
	--->	apple
	;	orange
	;	lemon.

:- func f(fruit) = string.
:- mode f(in) = out is semidet.
%:- mode f(out) = out is det.
f(apple) = "apple".

:- pred p(fruit).
:- mode p(out) is det.
p(orange).
% Or any set of fruit containing something for which f fails.
% You might prefer p(X):- (X = apple ; X = orange ; X = lemon).


main(!IO):-
	tst(A, B, C),
	io__write_string(A, !IO), io__nl(!IO),
	io__write_string(B, !IO), io__nl(!IO),
	io__write_string(C, !IO), io__nl(!IO).

:- pred tst(string, string, string).
:- mode tst(out, out, out) is det.
tst(A, B, C):-
	% yes:
	A = ( if some[Fruit] (
			p(Fruit),
			f(Fruit) \= f(Fruit)
		) then "yes" else "no" ),

	% yes:
	B = ( if some[Fruit] (
			p(Fruit),
			not(true1(f(Fruit)))
		) then "yes" else "no"),

	% no:
	C = ( if some[Fruit] (
			p(Fruit),
			not_true1(f(Fruit))
		) then "yes" else "no").

:- pred not_true1(string::in) is failure.
not_true1(X):- not true1(X).

:- pred true1(string::in) is det.
true1(_).
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------