[m-users.] Just saying thank you, determinism rocks.
Sean Charles (emacstheviking)
objitsu at gmail.com
Thu Jul 29 00:29:48 AEST 2021
Goats and gods, what a thread!
Thank you again Zoltan, that cleared up some points for me.
And, talking of rain gods and goats, it reminded me of this definition of involvement and commitment:
At a hog-roast, the chef is involved but the pig is committed.
Good day and thank you!
> On 28 Jul 2021, at 11:42, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
> 2021-07-28 20:05 GMT+10:00 "Volker Wysk" <post at volker-wysk.de>:
>>> I still have a few grey areas about cc_multi and cc_nondet
>> So do I...
> The basic idea is quite simple. Nondet and multi say that a predicate
> may have more than one solution, with nondet but not multi allowing
> zero solutions as well. A predicate mode which is nondet or multi
> will return all its solutions. If the mode is cc_nondet, that means
> "this mode of this predicate may have any number of solutions,
> but the implementation will stop after generating the first one,
> and in terms of the declarative semantics, it is unpredicatable
> which solution will be the first". Cc_multi is the same, except
> for disallowing zero solutions. Operationally, you *can*predict
> which solution will be the first, since Mercury does depth first search
> with a left-to-right execution, though not on the raw form of
> each clause body, but in its form after mode analysis reorders
> the clause body to put the producer of each variable before
> its consumer(s).
> How you can fit cc_multi code into det code, and cc_nondet code
> into semidet code, is only slightly more complicated. There are
> three ways:
> 1. You can declare main/2 to be cc_multi, in which case all the
> code it calls outside of a negated context may be cc_multi.
> 2. You can quantify away all the output variables of a cc_multi
> or cc_nondet computation. The different solutions of such
> computations differ only in the values of its output variables,
> so if you ignore all of them, the solutions are indistinguishable
> from the point of the caller. A cc_multi computation whose
> outputs are quantified away is det, while a cc_nondet computation
> with outputs quantified away is semidet.
> 3. The third way is the tricky one. If a computation can generate
> several solutions, but they are all equally good for your purposes,
> then you can tell the compiler that, using a promise_equivalent_solutions
> scope. For example, if the computation returns a list, but you care
> only about the set of items in it, and not their order or their multiplicity,
> then [1, 2], [2, 1] and [1, 2, 2, 1] are equivalent, and it does not matter
> which one you get. The *reason* this is a bit tricky in practice is that
> (a) you have to have in your mind an "equality theory" that partitions
> the space of outputs in a set of partitions, so that all solutions in a partition
> are equivalent, and then (2) write the *rest* of the program in such a way
> that it actually produces the same output no matter which element
> from a given equivalence class you give it. Getting this right is up to you.
> The compiler does not know your equality theory, and therefore
> cannot help you. (Actually, even if it did know, helping would require
> a full fledged theorem prover.)
> The compiler *can* help you if you write code that asks cc_multi/cc_nondet
> code to generate more than one solution. If say p is cc_multi, while q is
> semidet, then the conjunction "p, ..., ..., q" won't work, because if q fails,
> execution would have to backtrack to p to ask it to generate a second
> solution, but cc_multi/cc_nondet predicates cannot do that. However,
> in such cases, the compiler will tell you where the error is.
>>> but I can live with that. Basically I sat and wrote down some study goals
>>> and then over the last 23 days (according to my project diary) I’ve been
>>> poking and prodding the compiler by writing a `det` predicate and then
>>> breaking it, unbreaking it etc etc.
>>> In the last week I have made fantastic progress with my language project,
>>> I look forward to compiler errors. It’s a FANTASTIC language as I always
>>> knew it would turn out to be
>> Yes, Mercury's the real thing. In comparison, languages like Java and Python
>> look rather ridiculous. :)
> I have a file of interesting quotes I have gathered over the years, mostly
> from usenet news groups (when they were still a thing). One, from probably
> around a quarter of a century ago, is relevant here. It goes like this:
> Of course SML does have its weaknesses, but by comparison, a discussion of
> C++'s strengths and flaws always sounds like an argument about whether one
> should face north or east when one is sacrificing one's goat to the rain god.
>>> Thanks again.
>> You're welcome.
> Let me add a "you're welcome" from the Mercury team as well.
More information about the users