3
$\begingroup$

I want to understand general method for formally defining non-deterministic algorithm. But all formal definitions I see are related to FSM/Turing-machines.

What is the reference for non-deterministic computations in context of Kleene's general recursion or just generic (semi-)decidable relations or similar formalisms?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Why do you assume there is such a definition? $\endgroup$
    – Emil Jeřábek
    Commented Aug 4, 2023 at 14:38
  • $\begingroup$ I have seen its usage in non-formal arguments, so I believe it could be formalized. Another reason is that various simple results on semi-decidable relations seems to be similar to notion of non-deterministic algorithm. $\endgroup$
    – uhbif19
    Commented Aug 4, 2023 at 14:53
  • 1
    $\begingroup$ Why, of course it can be formalized: it is formalized by nondeterministic Turing machines. Typically, the need for nondeterministic algorithms comes up in the context of computational complexity, where it’s extremely inconvenient (if not impossible) to formalize algorithms by means of general recursive functions, and where the standard model of computation is multitape Turing machines. But nothing stops you from, say, formalizing nondeterministic recursive functions $f(\vec x)$ by means of deterministic recursive functions $f(\vec x,y)$ where $y$ represents the nondeterministic choices. $\endgroup$
    – Emil Jeřábek
    Commented Aug 4, 2023 at 15:04
  • 1
    $\begingroup$ Because recursive function have no natural analogue of common resource measures such as time and space. $\endgroup$
    – Emil Jeřábek
    Commented Aug 4, 2023 at 21:19
  • 2
    $\begingroup$ @EmilJeřábek: lambda-the-ultimate.org/node/5021 $\endgroup$
    – Andrej Bauer
    Commented Aug 5, 2023 at 7:46

2 Answers 2

Reset to default
2
$\begingroup$

You could easily make Kleene's $\mu$-recursive programs nondeterministic. A $\mu$-recursive program consists of a sequence of function symbols, each defined from previous ones by composition, primitive recursion, or minimization (the $\mu$-operator). Simply add a fourth operator: nondeterministic choice. Something like $$ f = \mathrm{choose}(g,h)$$ meaning, $f$ is defined to be either $g$ or $h$ nondeterministically. I'm sure there are other ways to add nondeterminism as well. (For example, replacing $\mu$, the least witness operator, by something which nondeterministically selects some witness if it exists.)

That said, it's unclear that such a programming language would be interesting. Extensionally, adding nondeterministic choice does not increase the expressive power of $\mu$-recursive programs. Intensionally, I don't see how to recover interesting resources (like nondeterministic time on a TM) from this model. That's not to say that there's definitely nothing there, but I doubt there's a reference!

Improve this answer
$\endgroup$
3
  • $\begingroup$ > Simply add a fourth operator: nondeterministic choice That forces to move from partial functions into functions returning set of values. And it is not entirely clear to me that this does not break anything. Also I am not sure that angelic/demonic stuff is not important here. > Extensionally, adding nondeterministic choice does not increase the expressive power of μ-recursive programs I think one could define semi-decidable sets that way, AFAIU. $\endgroup$
    – uhbif19
    Commented Aug 7, 2023 at 19:32
  • $\begingroup$ Sure, nondeterministic models of computation typically compute something more complicated than a partial function. So when I say "does not increase expressive power," I mean "does not compute more partial functions." I'm not sure what angelic/demonic stuff is? Also, how would you "define" (I assume you mean "decide"?) semidecidable sets? $\endgroup$
    – Siddharth
    Commented Aug 7, 2023 at 22:37
  • $\begingroup$ > I'm not sure what angelic/demonic stuff is? AFAIU, angelic/demonic non-determinism is way of interaction on non-deterministic choice with non-terminating programs, so should be related lazy/eager semantics. > how would you "define" (I assume you mean "decide"?) semidecidable sets? Sets which are generated with non-deterministic function. Of course that does mean that non-deterministic functions may return infinite set of results by running infinitely. $\endgroup$
    – uhbif19
    Commented Aug 10, 2023 at 18:21
-1
$\begingroup$

While, this does not fully answer my question, it seems like "guess-and-verify" translation makes this question less important. Because defining "verification problem" does not depend on computation formalism, thus clearly works for recursive functions.

It does cover one of the motivations for my question. On wikipedia page for "propositional proof system" there is a claim "One can view the second definition as a non-deterministic algorithm for solving membership in TAUT", which was unclear to me. Looks like it is just informal usage for such "non-determinism to verification" translation, so it does not require formal non-determinism definition.

Another (non-formal) complication I see is that non-determinism is (at least in formalizations which I have seen) related to small-step semantics, while recursive functions are essentially big-step.

AFAIU, they define set of computable functions, but "forget" computation steps of their execution, just like big-step semantics do. This should make defining of "number of non-deterministic choices" more complicated.

Thus verification formalism seems much better fit for recursion formalisms. Not only that, it seems like size of proof certificate essentially encodes number of non-deterministic choices taken.

It may be that papers on non-determinism in FP should be more relevant then internalizing choice operator into (general) recursion formalism.

One Two

Improve this answer
$\endgroup$
4
  • $\begingroup$ Why are recursive functions essentially big-step? $\endgroup$
    – cody
    Commented Aug 7, 2023 at 20:50
  • $\begingroup$ And why is big-step more deterministic? $\endgroup$
    – cody
    Commented Aug 7, 2023 at 20:50
  • $\begingroup$ I mean that recursion formalisms, AFAIK, give you set of commutable functions and (semi-)computable sets, but no reduction/step semantics. This to me seems similar to how big-step semantics is defined: inductively define program results, forgetting internal computation steps. While it probably should be possible to specify such reduction semantics, I did not seen use of such so far. Also recursion/search combinators AFAIU are defined to work in single step, while usually small-step semantic perform recurstion/cycles one iteration in a time. This should probably complicate things. $\endgroup$
    – uhbif19
    Commented Aug 10, 2023 at 17:58
  • $\begingroup$ > And why is big-step more deterministic? You would probably need to number of performed non-deterministic choices. Such cost calculations seems to be more naturally related to small-step semantics. $\endgroup$
    – uhbif19
    Commented Aug 10, 2023 at 18:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.