RC: Semantics of Totality

[paulch42]

VDM allows a function to be specified as total, but the semantics of total functions are not clearly defined. There seems to be two schools of thought. Consider the function

f[@a,@b]: @a +> @b
f(x) == …x…
pre P(x)
post Q(x,RESULT);

The meaning is either

1. given a value a of type @a such that P(a) holds, evaluation of the expression f(a) computes to a value b of type @b such that Q(a,b) holds.

or

2. given a value a of type @a, evaluation of the expression f(a) computes to a value b of type @b such that Q(a,b) holds if P(a) holds.

The difference relates to elements a from the domain for which P(a) does not hold. In the first case no value is defined; the definition need not include cases for argument values that do not satisfy P. In the second case a value must be computed, but it can be an arbitrary element of @b.

A more concrete example

map_apply[@a,@b]: map @a to @b * @a +> @b 
map_apply(m,x) == m(x)
pre x in set dom m;

By interpretation 1 this definition is well-defined. By interpretation 2 it is not well-defined since it does not compute a value for those elements of @a not in the domain of m.

The semantics of totality needs to be clarified and documented.

[nickbattle]

Didn't we discuss this with PGL a while ago (while I was still at Fujitsu)? I thought we decided that totality was with respect to preconditions - which I took to mean case 1. Looking at the POs that get generated for satisfiability, they start with "pref(args) => ...". So if the precondition is not met, there is no obligation to do anything in particular. This is case 1 again.

Of course that's no reason not to clarify it (whichever case is correct) :-)

[paulch42]

You, me and PGL did discuss this via email quite a while ago and the result was as you said. More recently there was a discussion in core and I got the impression from that it was not so clear, but that may just have been me.

Thought I would raise it so we can be definitive and then document it in the LRM.

I agree that case 1 seems the correct interpretation. If I impose a pre-condition on a function I am saying from a specification perspective that I don’t care what happens if the argument does not satisfy the pre-condition, so I need not provide a case in the function definition that accounts for arguments that do not satisfy the pre-condition (i.e. it is total for the domain of interest).

On 23 Nov 2017, at 2:33 am, Nick Battle notifications@github.com wrote:

Didn't we discuss this with PGL a while ago (while I was still at Fujitsu)? I thought we decided that totality was with respect to preconditions - which I took to mean case 1. Looking at the POs that get generated for satisfiability, they start with "pref(args) => ...". So if the precondition is not met, there is no obligation to do anything in particular. This is case 1 again.

Of course that's no reason not to clarify it (whichever case is correct) :-)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/overturetool/language/issues/45#issuecomment-346385458, or mute the thread https://github.com/notifications/unsubscribe-auth/AQisRon3UKy16YcChA-nssfGQETamfKoks5s5D6ugaJpZM4Qj8WQ.

[peterwvj]

I agree. Totality with respect to pre-conditions seems correct (case 1). Surely we can update the LRM to make that more clear.

[nickbattle]

As I see it, in effect, the precondition qualifies the domain of the function. Then totality is defined with respect to that restricted domain. If we're agreed, then that should be clarified in the LRM.

[paulch42]

Proposal for LRM update to be inserted at end of section 6.27.

---

When a function is defined to be total, that totality is with respect to the pre-condition. Consider an alternative definition of ‘f’

f: nat * nat +> nat f(m,n) == m div n pre n <> 0;

The definition states the function is total for all values of type nat*nat where the second element of the pair is non-zero. Therefore, even though the function is not defined for values such as mk_(4,0) it is still a total function. On the other hand, the definition

f: nat * nat +> nat f(m,n) == m div n;

is incorrect because it is not defined for values such as mk_(4,0) hence not total.

---

I think we also need a correction in section 3.5. It is stated

If an ord clause is defined, three new (total) functions are created implicitly with the signatures:

The relation must be a strict partial order, but it need not be total, so ‘(total)’ should be removed.

Also at end of P.35, replace ‘..’ with ‘.’

On 24 Nov 2017, at 11:51 pm, Nick Battle notifications@github.com wrote:

As I see it, in effect, the precondition qualifies the domain of the function. Then totality is defined with respect to that restricted domain. If we're agreed, then that should be clarified in the LRM.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/overturetool/language/issues/45#issuecomment-346822239, or mute the thread https://github.com/notifications/unsubscribe-auth/AQisRg-aaTIVpBBCdnke3SjYBoyFMYWtks5s5rvigaJpZM4Qj8WQ.

[tomooda]

Done. Please check https://github.com/overturetool/documentation/blob/editing/documentation/VDM10LangMan/VDM10_lang_man.pdf and close this if the new LRM looks OK.

[peterwvj]

As Paul pointed out in his email, this issue can be closed.