<p>You could easily make Kleene's <span class="math-container">$\mu$</span>-recursive programs nondeterministic. A <span class="math-container">$\mu$</span>-recursive program consists of a sequence of function symbols, each defined from previous ones by composition, primitive recursion, or minimization (the <span class="math-container">$\mu$</span>-operator). Simply add a fourth operator: nondeterministic choice. Something like
<span class="math-container">$$ f = \mathrm{choose}(g,h)$$</span>
meaning, <span class="math-container">$f$</span> is defined to be either <span class="math-container">$g$</span> or <span class="math-container">$h$</span> nondeterministically. I'm sure there are other ways to add nondeterminism as well. (For example, replacing <span class="math-container">$\mu$</span>, the least witness operator, by something which nondeterministically selects some witness if it exists.)</p>
<p>That said, it's unclear that such a programming language would be interesting. Extensionally, adding nondeterministic choice does not increase the expressive power of <span class="math-container">$\mu$</span>-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 <em>definitely</em> nothing there, but I doubt there's a reference!</p>

CC BY-SA 4.0
2023-08-07T19:32:08.697Z
> 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.
uhbif19
CC BY-SA 4.0
2023-08-07T22:37:54.737Z
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?
Siddharth
CC BY-SA 4.0
2023-08-10T18:21:38.720Z
> 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.
uhbif19
CC BY-SA 4.0
2023-08-07T16:30:34.403Z
2023-08-07T16:30:34.403Z
Siddharth
<p>While, this does not fully answer my question, it seems like <a href="https://cs.stackexchange.com/questions/58154/how-does-nondeterministic-time-relate-to-verifiability">&quot;guess-and-verify&quot; translation</a> makes this question less important. Because defining &quot;verification problem&quot; does not depend on computation formalism, thus clearly works for recursive functions.</p>
<p>It does cover one of the motivations for my question. On <a href="https://en.wikipedia.org/wiki/Propositional_proof_system" rel="nofollow noreferrer">wikipedia page for &quot;propositional proof system&quot;</a> there is a claim &quot;One can view the second definition as a non-deterministic algorithm for solving membership in TAUT&quot;, which was unclear to me. Looks like it is just informal usage for such &quot;non-determinism to verification&quot; translation, so it does not require formal non-determinism definition.</p>
<hr />
<p>Another (non-formal) complication I see is that non-determinism is (at least in formalizations which I have seen) related to <a href="https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html" rel="nofollow noreferrer">small-step semantics</a>, while recursive functions are essentially big-step.</p>
<p>AFAIU, they define set of computable functions, but &quot;forget&quot; computation steps of their execution, just like big-step semantics do. This should make defining of &quot;number of non-deterministic choices&quot; more complicated.</p>
<p>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.</p>
<hr />
<p>It may be that papers on non-determinism in FP should be more relevant then internalizing choice operator into (general) recursion formalism.</p>
<p><a href="https://watermark.silverchair.com/35-5-514.pdf?token=AQECAHi208BE49Ooan9kkhW_Ercy7Dm3ZL_9Cf3qfKAc485ysgAAA1UwggNRBgkqhkiG9w0BBwagggNCMIIDPgIBADCCAzcGCSqGSIb3DQEHATAeBglghkgBZQMEAS4wEQQMj_FQ68-FPL9l_8ytAgEQgIIDCHsaWP5sJXeEUJAo3aLp97toH9StEvJHF8VGwQSs2RL5BD9uVJYYASN-NnKtwYPFOeiD5hWxogLYu9F0Clh0act5JKhu6RkflrJuTzUfFfyORv9IIv-325EkoE4JX1FvlKlWTrqBFGgFQVQZwysyyo0HTak4izFSNDf01onkECi-vdITH_bdCP_Ky1RK2P_a3TW-LOrvkhjL5M62W724oxn2kSQPm_zmuGyblt0I2x764EpXn6yQHnB3vnpoQW7MLMRvL7jkLLfztjQlkEFxci7-d4HlRz9iETZkIjchcpF3pJeDegKX8Shkmpkeke-VgRTIsYyYSBsLnTfHzMcacnQjQthQvZRj7029Ibd-Yrb6HZwj-vw4xA06VFcFPMnEIllQg8_-FcoML7JFFXV2SjMI34-SMJN6gFBf89VIUuFOxrfxuuN-VUBdxIPz7iZg4PgWbi7sRf_5FuyEiz_wfip_5C-jf7VBDrsqBu8QBJpLaSVxTf_KUiQ-ghgPKBfxQrRoThKPQ_SdxXPCtPocnZY1oIAN86WJXOzw0wbpJnXh0C-izT82ZUqOUmliALZLrhv9HTAeeRAYno8F83NmkFvMV4s_rsdC6R-LADyA_nZ8q1x4y16GA2RNyU2MSyoj-QLpbjKkPnqdHv8zlwswDX20pEuocwq9krNuAs0Bft6mC2wpqTDvWS86TH1YNjYRufCp3H1TsUfldQOATprCWe9txfKnr4mYnWFZVOud97teE_vYCvqGxGk0fvtDj-zqiVKMrcO214xf6Ngd6g2T1F2sd9Kb9fp7EJg1lmozBnfipNjzbaSQr273_gEjkXWQZfLJvE3f7m5DJ6afyPZCe3pmXSWndh_I58vQhAvZmvCH1hT2rsXS_GtHrVix_FKl5jc9ngmXLFiowkJsNVZtntZh80T-I8pKQKfdpN8oM-q2WDdsnuL4rj4WZHuHZoUoSTu0Lt_SoO-Ov2fpFCxs2p5BPVADmXc7u8Lm3omjy-rlPM_ygDjM7ZKomoPOyoeDe55u511ICuRG" rel="nofollow noreferrer">One</a>
<a href="https://link.springer.com/chapter/10.1007/978-1-4471-3166-3_21" rel="nofollow noreferrer">Two</a></p>

CC BY-SA 4.0
2023-08-07T20:50:07.137Z
Why are recursive functions essentially big-step?
cody
CC BY-SA 4.0
2023-08-07T20:50:42.050Z
And why is big-step more deterministic?
cody
CC BY-SA 4.0
2023-08-10T17:58:43.097Z
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.
uhbif19
CC BY-SA 4.0
2023-08-10T18:04:00.297Z
> 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.
uhbif19
CC BY-SA 4.0
2023-08-04T18:19:40.793Z
2023-08-10T18:27:37.223Z
2023-08-10T18:27:37.223Z
uhbif19
<p>I want to understand general method for formally defining non-deterministic algorithm. But all formal definitions I see are related to FSM/Turing-machines.</p>
<p>What is the reference for non-deterministic computations in context of Kleene's general recursion or just generic (semi-)decidable relations or similar formalisms?</p>

CC BY-SA 4.0
2023-08-04T14:38:06.053Z
Why do you assume there is such a definition?
Emil Jeřábek
CC BY-SA 4.0
2023-08-04T14:53:50.150Z
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.
uhbif19
CC BY-SA 4.0
2023-08-04T15:04:49.840Z
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.
Emil Jeřábek
CC BY-SA 4.0
2023-08-04T18:17:13.530Z
> where it’s extremely inconvenient (if not impossible) to formalize algorithms by means of general recursive functions

Why so?
uhbif19
CC BY-SA 4.0
2023-08-04T21:19:17.107Z
Because recursive function have no natural analogue of common resource measures such as time and space.
Emil Jeřábek
CC BY-SA 4.0
2023-08-05T07:46:43.370Z
@EmilJeřábek: http://lambda-the-ultimate.org/node/5021
Andrej Bauer
<computability><turing-machines><nondeterminism><recursion>
What is formal definition of non-deterministic algorithm in context of primitive/general recursion?
uhbif19
# What is formal definition of non-deterministic algorithm in context of primitive/general recursion?

(Asked by: username_0 on 2023-08-04)

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?

**Tags:** computability, turing-machines, nondeterminism, recursion

> **Comments:**
> **username_1**: Why do you assume there is such a definition?  
> **username_0**: 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.  
> **username_1**: 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.  
> **username_0**: > where it’s extremely inconvenient (if not impossible) to formalize algorithms by means of general recursive functions  Why so?  
> **username_1**: Because recursive function have no natural analogue of common resource measures such as time and space.  
> **username_2**: @EmilJeřábek: http://lambda-the-ultimate.org/node/5021  

---

## 2 answers

### Answer by username_3 on 2023-08-07. Score: 2

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!

> **Comments:**
> **username_0**: > 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.  
> **username_3**: 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?  
> **username_0**: > 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.  

---

### Answer by username_0 on 2023-08-04. Score: -1

While, this does not fully answer my question, it seems like ["guess-and-verify" translation](https://cs.stackexchange.com/questions/58154/how-does-nondeterministic-time-relate-to-verifiability) 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"](https://en.wikipedia.org/wiki/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](https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html), 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](https://watermark.silverchair.com/35-5-514.pdf?token=AQECAHi208BE49Ooan9kkhW_Ercy7Dm3ZL_9Cf3qfKAc485ysgAAA1UwggNRBgkqhkiG9w0BBwagggNCMIIDPgIBADCCAzcGCSqGSIb3DQEHATAeBglghkgBZQMEAS4wEQQMj_FQ68-FPL9l_8ytAgEQgIIDCHsaWP5sJXeEUJAo3aLp97toH9StEvJHF8VGwQSs2RL5BD9uVJYYASN-NnKtwYPFOeiD5hWxogLYu9F0Clh0act5JKhu6RkflrJuTzUfFfyORv9IIv-325EkoE4JX1FvlKlWTrqBFGgFQVQZwysyyo0HTak4izFSNDf01onkECi-vdITH_bdCP_Ky1RK2P_a3TW-LOrvkhjL5M62W724oxn2kSQPm_zmuGyblt0I2x764EpXn6yQHnB3vnpoQW7MLMRvL7jkLLfztjQlkEFxci7-d4HlRz9iETZkIjchcpF3pJeDegKX8Shkmpkeke-VgRTIsYyYSBsLnTfHzMcacnQjQthQvZRj7029Ibd-Yrb6HZwj-vw4xA06VFcFPMnEIllQg8_-FcoML7JFFXV2SjMI34-SMJN6gFBf89VIUuFOxrfxuuN-VUBdxIPz7iZg4PgWbi7sRf_5FuyEiz_wfip_5C-jf7VBDrsqBu8QBJpLaSVxTf_KUiQ-ghgPKBfxQrRoThKPQ_SdxXPCtPocnZY1oIAN86WJXOzw0wbpJnXh0C-izT82ZUqOUmliALZLrhv9HTAeeRAYno8F83NmkFvMV4s_rsdC6R-LADyA_nZ8q1x4y16GA2RNyU2MSyoj-QLpbjKkPnqdHv8zlwswDX20pEuocwq9krNuAs0Bft6mC2wpqTDvWS86TH1YNjYRufCp3H1TsUfldQOATprCWe9txfKnr4mYnWFZVOud97teE_vYCvqGxGk0fvtDj-zqiVKMrcO214xf6Ngd6g2T1F2sd9Kb9fp7EJg1lmozBnfipNjzbaSQr273_gEjkXWQZfLJvE3f7m5DJ6afyPZCe3pmXSWndh_I58vQhAvZmvCH1hT2rsXS_GtHrVix_FKl5jc9ngmXLFiowkJsNVZtntZh80T-I8pKQKfdpN8oM-q2WDdsnuL4rj4WZHuHZoUoSTu0Lt_SoO-Ov2fpFCxs2p5BPVADmXc7u8Lm3omjy-rlPM_ygDjM7ZKomoPOyoeDe55u511ICuRG)
[Two](https://link.springer.com/chapter/10.1007/978-1-4471-3166-3_21)

> **Comments:**
> **username_4**: Why are recursive functions essentially big-step?  
> **username_4**: And why is big-step more deterministic?  
> **username_0**: 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.  
> **username_0**: > 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.  

---

