> My specific concern is that by having logical semantics in a language you can represent non-deterministic ambiguous computations

As I understand it the verse calculus can only represent non-deterministic unambiguous computations, and that follows from confluence. The point is that it's the non-determinism that's useful, not ambiguity. Am I understanding correctly?

The paper has this to say:

> Choice is a fundamental feature of all functional logic languages. In VC, choice is expressed in the syntax of the term (“laid out in space”) rather than, as is more typical, handled by non-deterministic rewrites and backtracking (“laid out in time”). This makes VC completely deterministic, unlike most functional logic languages which are non-deterministic by design (Section 6.1).

So, the language is deterministic which is a result of being confluent. And going to section 6.1 as suggested says this:

> In contrast, our rules never pick one side or the other of a choice. And yet, (3 +(20 | 30)) can still make progress by floating out the choice (rule choose in Fig. 3), thus (3 +20) | (3 +30). In effect, choices are laid out in space (in the syntax of the term), rather than being explored by non-deterministic selection. Rule choose is not a new idea.

So the syntax is "ambiguous" and given context with "choose" to make it unambiguous.

To answer your question more plainly it's the ambiguity that's important. Non-determinism usually follows as a natural consequent.

However, it may be a hinderance or it may be desired. Usually we're only interested in one single useful result. But, if I do a search in a data structure for all occurrences of X, and there are 5 of them then I may want a result of all 5 occurrences of X.

> So, the language is deterministic which is a result of being confluent. And going to section 6.1 as suggested says this:

Non-determinism in programming language theory does not mean _physical_ non-determinism.

> To answer your question more plainly it's the ambiguity that's important. Non-determinism usually follows as a natural consequent.

Non-determinism in programming language theory does not require ambiguity. Non-determinism here means something more like that the program's execution will search for matching solutions as if it knew them non-deterministically, but the search process will be deterministic (and it's almost invariably a depth-first search).

I can't speak to the point of doing this, but (IIRC/IIUC) you're talking paths and they're talking the entire computation tree, i.e., a term in their calculus represents all solutions, and computing normal forms makes them easy to read off (?). Perhaps there's some meat in how they handle the equivalent of `bagof/3`/`setof/3`.