| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000343 | mercury | Bug | public | 2014-07-01 05:43 | 2014-07-02 10:07 | ||||
| Reporter | aeonioshaplo | ||||||||
| Assigned To | pbone | ||||||||
| Priority | high | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | no change required | ||||||
| Product Version | |||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0000343: Termination checking incorrect for disjunction | ||||||||
| Description | In certain cases where prolog-style logic programming is used, mmc will infer that a recursive pred like fib is multi or nondet when it should be det, especially when dealing with disjunctions. | ||||||||
| Steps To Reproduce | attempt to compile the attached examples fib_naive.m and fib_tail.m. | ||||||||
| Additional Information | I'm including a third file, philosophy.m, which demonstrates a case where termination checking produces correct results against disjunction. In particular, writeStringsWithNLs/3 is of the same form as the above fib programs which cause it to fail. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
juliensf (administrator) 2014-07-01 13:02 |
In fib_naive.m, the clause fib(In, Out) :- ... will also match either fib(0, 0) or fib(1, 1), so the compiler is correct, the disjunction of those clauses is multi rather than det. Likewise, for fib_tail where any input could match either of the two clauses given. That is not the case for writeStringsWithNLs/3, where the first clauses will only match inputs with an empty list and the second will only match inputs with a non-empty list. In short, the compiler is correct here. |
|
aeonioshaplo (reporter) 2014-07-01 13:33 |
I don't believe that is correct, for example fib_naive could be stated equivalently as: fib(In, Out) :- In is 0, Out is 0 ; In is 1, Out is 1 ; fib(In - 1, X), fib(In - 2, Y), Out is X + Y. which are mutually exclusive and will only ever bind Out to one value in a given recursion. If both modes were ::out then it would be multi, but since one of the modes is ::in it should not be. |
|
juliensf (administrator) 2014-07-01 13:51 |
They are not mutually exclusive, if 'In' is 0, both the first clause will "succeed" and the third. (Operationally, it will probably go into loop due to 'In' being negative in the recursive call, but that's not something determinism analysis deals with.) By declaring this predicate to be 'det' you have effectively told the compiler that this will not be the case, hence the error. An actually det version of fib in Mercury would be written as follows: fib(In, Out) :- ( if In = 0 then Out = 0 else if In =1 then Out = 1 else fib(In - 1, X), fib(In -2 , Y), Out = X + Y ). |
|
juliensf (administrator) 2014-07-01 13:57 |
For further information, see the Prolog to Mercury transition guide, <http://www.mercurylang.org/information/doc-latest/mercury_trans_guide/index.html>. |
|
aeonioshaplo (reporter) 2014-07-01 14:32 Last edited: 2014-07-01 14:34 |
I figured this out. This isn't a determinacy checking issue, it's a mode checking issue and the determinacy problem is just a symptom. By declaring that In has mode ::in, I am stating that In should always be ground when the function is called (or I should get errors otherwise) and therefore the two unifications "X is 0" and "X is 1" can only be -comparisons- and not assignments. However, the compiler is inferring the other way around, and if you view them as assignments it makes sense that it would infer multi or nondet instead of det. Also, if-then-else should not be required in logic since if A then B else C is in most cases equivalent to head :- A, B; C. which is more convenient and natural to write in a logic language. In cases where it isn't equivalent, mercury currently still makes it (more or less) equivalent by default. (referring to conjunctions with predicates that have !IO modes, which it refrains from reordering) >>They are not mutually exclusive, if 'In' is 0, both the first clause will "succeed" and the third. That's not how logic is supposed to work, AFAIK. If I write, for example: head :- A; B; C. B should only be evaluated if A fails, and C should only be evaluated if both A and B fail. If A succeeds B and C should never be called. Thus, an equivalent statement where C is evaluated would be: head :- not(A ; B), C. or head :- not(A), not(B), C. To be fair, it took me a pretty long time to understand the nuances of logic that well. |
|
aeonioshaplo (reporter) 2014-07-01 16:48 |
Nevermind, you were right and I was wrong. I forget that logical 'or' is not xor, and '0-1' does in fact produce a perfectly valid solution when the type is 'int'. That makes me wonder how the prolog version ever worked. I can also see how if-then-else is useful, although I'm not entirely satisfied with that syntax. Or maybe just with the lack of an exclusive switch. I can't think of any more elegant way of avoiding the need for explicit negations, anyway. At any rate I'd say it's safe to call this resolved, or failing that 'confused' works too. :P |
|
pbone (administrator) 2014-07-02 10:06 |
A possible point of confusion is that Mercury does support switches when a variable is unified with a distinct function symbol in each arm of a disjunction then the disjunction is a switch (exclusive). For example: ( X = a, ... ; X = b, ... ). However this currently does not work for numbers (it probably should) and often confuses new programmers. Additionally the compiler does not yet understand that comparisons can form exclusive and complete checks. Eg this doesn't work: ( X > 0, ... ; X =< 0, ... ). Also if you dislike the if-then-else syntax then there's another syntax: http://www.mercurylang.org/information/doc-release/mercury_ref/Goals.html#Goals Thanks. |
|
pbone (administrator) 2014-07-02 10:07 |
Not a bug. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2014-07-01 05:43 | aeonioshaplo | New Issue | |
| 2014-07-01 05:43 | aeonioshaplo | File Added: examples.tar.gz | |
| 2014-07-01 13:02 | juliensf | Note Added: 0000723 | |
| 2014-07-01 13:33 | aeonioshaplo | Note Added: 0000724 | |
| 2014-07-01 13:51 | juliensf | Note Added: 0000725 | |
| 2014-07-01 13:57 | juliensf | Note Added: 0000726 | |
| 2014-07-01 14:32 | aeonioshaplo | Note Added: 0000727 | |
| 2014-07-01 14:34 | aeonioshaplo | Note Edited: 0000727 | View Revisions |
| 2014-07-01 16:48 | aeonioshaplo | Note Added: 0000728 | |
| 2014-07-02 10:06 | pbone | Note Added: 0000729 | |
| 2014-07-02 10:07 | pbone | Note Added: 0000730 | |
| 2014-07-02 10:07 | pbone | Status | new => closed |
| 2014-07-02 10:07 | pbone | Assigned To | => pbone |
| 2014-07-02 10:07 | pbone | Resolution | open => no change required |
| Issue History |