CiaoPP: `trust' and determinism

[simonefulvio-rollini]

Hello,

I am trying to perform determinacy checking on the following example:

:- module(test16, [p1/2], [assertions,nativeprops]).

:- entry p1(X, W) : (num(X), var(W)).
:- check success p1(X, W) : (num(X), var(W)) => num(W).
:- check comp p1(X, W) : (num(X), var(W)) + det.

p1(X, W):-
    p2(X, Z),
    W is 2 * Z.

:- trust pred p2(X, Z) : (num(X), var(Z)) => num(Z) + det.
:- impl_defined(p2/2).

The answer returned by CiaoPP is:

{WARNING (ctchecks_pred_messages): (lns 5-5) Could not verify assertion:
:- check comp p1(X,W)
   : ( num(X), var(W) )
   + det.
because
    multi
could not be derived from inferred comp:
[det]          is_det,mut_exclusive 
[eterms]       num(X),num(W) 
[shfr]         ground([X,W]) 
[generic_comp] [No info available]
}

However, verification is successful both when replacing 'det' with 'semidet' and with 'multi' in p1 check:

{NOTE (ctchecks_pred_messages): (lns 5-5) Verified assertion:
:- check comp p1(X,W)
   : ( num(X), var(W) )
   + semidet.
}

{NOTE (ctchecks_pred_messages): (lns 5-5) Verified assertion:
:- check comp p1(X,W)
   : ( num(X), var(W) )
   + multi.
}

Looking at the documentation on determinacy properties, I cannot understand the tool behavior:

• What information is missing in order for CiaoPP to prove that the predicate p1 is deterministic?
• Is it not the case that the conjunction of 'semidet' and 'multi' is equivalent to 'det'?
• What is the difference respectively between the predicates 'is_det' and 'semidet', 'multi' and 'not_fails', 'nondet' and 'possibly_nondet'? Does 'non_det' require at least two solutions to succeed?

Thanks for the help,
Simone

[mherme]

Hi Simone, also if you just change det to semidet in the assertion for p1/2 it works. The problem is that det means exactly one solution, i.e., it requires guaranteeing that the predicate will not fail. This means that det requires performing non-failure analysis, which the CiaoPP analyzer can do, but the 'auto' mode in analysis selection is not turning it on. You can go into the CiaoPP menu, in 'Abstract domain selection' put it in manual mode, and then in 'Non failure' select 'nfdet', which performs combined non-failure and determinacy analysis. Let us know if it works for you!

[simonefulvio-rollini]

Hi Manuel, thank you, that is exactly what I was missing: explicitly setting the abstract domains allowed me to solve all the problems where the tool could prove 'semidet' and 'multi', but not 'det'.

[pedro-lopez-garcia]

Hi Simone,

Is it not the case that the conjunction of 'semidet' and 'multi' is equivalent to 'det'?

Exactly, yes.

What is the difference respectively between the predicates 'is_det' and 'semidet',

They are equivalent. The difference is purely syntactic: 'is_det' is the
property name used in our initial CiaoPP implementation, while 'semidet'
is the property name used in Mercury. We kept both names for backward
compatibility, but we plan to unify them under 'semidet' in the future.

'multi' and 'not_fails',

The same applies here: the two properties are equivalent, with 'multi'
being the name used in Mercury. They will be unified under 'multi'.

'nondet' and 'possibly_nondet'?

Again, the same applies, with 'nondet' being the name used in Mercury.

Does 'non_det' require at least two solutions to succeed?

Yes, that is its meaning.

Best regards,

[simonefulvio-rollini]

Hi Pedro, thank you, my doubts have been clarified.