Infinite Loop on Self-Negating Recursive Definition Without Feedback or Timeout

[LEARNTAU]

1. Summary

   • Description: When defining a recursive function such that a call refers to its own negation, Tau enters what seems to be an infinite normalization loop with 100% CPU usage. The REPL becomes unresponsive, and there's no output or way to interrupt the evaluation.

2. Environment

   • Tau Version: for now "v0.7-alpha (e7e7ab9)"
   • Build Number or Date:
   • Operating System: Ubuntu

3. Steps to Reproduce
   Step 1: g[0](y) := 0
   Step 2: g[n](y) := g[n](y)'
   Step 3: n g[5](1)

   Expected Result
   Tau should either:

• Detect self-referential

• Abort normalization after a timeout

• Provide a warning about non-terminating behavior

• Allow the user to interrupt execution

  Actual Result

• Tau becomes unresponsive

• No error or feedback is given

• CPU spikes to 100%

• User cannot break or cancel the operation via REPL input

4. Additional Information
   • Screenshots:

5. Severity and Impact
   Severity Level:*

• Impact on System Stability (High): It causes the REPL to hang indefinitely and maxes out CPU. That’s a serious impact on usability. On large-scale deployments or future integrations (like APIs or real-time environments), this could crash processes or hog system resources.

• Ease of Triggering (Very Easy): A user just has to define a self-negating function. No deep knowledge required. This makes it potentially abusable by bad actors or just accidental by curious users.

• Frequency (Occasional but probable): Not everyone will write self-negating functions, but it's a kind of mistake that an experimental or beginner user could make easily, especially when playing with recursive definitions.

• Visibility / Feedback (Very Low): No error message, no warning, no timeout, no way to cancel. This makes the problem feel like a freeze or crash, even though the system is just stuck in a logical loop.

• Security Concern (Optional) Medium: While it’s not a security bug per se, it could be used as a vector for resource exhaustion. If the REPL were exposed in a web service or future TauNet node, attackers could overload it with such queries.

Impact on Work:

• Degrades user experience
• Risk of unintentional infinite loops
• Possible vector for DoS-like attacks

Suggested Improvements:

• Add loop detection or termination heuristics
• Implement a timeout or resource cap
• Allow interrupt commands in REPL (e.g., Ctrl+C or :cancel)
• Provide real-time feedback during long evaluations

6. Workaround (if applicable)

   • Tell us if you found a way around this problem:

7. Contact Information

   • Name: @LEARNTAU
   • Email:
   • Additional Notes:

Submission Instructions

• Make sure to attach any input files to this bug report.

[LEARNTAU]

Workaround

I tried to change g[0](y) := 0 to g[0](y) := F

then when I repeat the same procedure, the Tau REPL does not hang anymore but see the error.

But if I exit the Tau REPL and do the same thing again without changing 0 to F
g[0](y) := 0
g[n](y) := g[n](y)'
n g[5](1)

same problem occur.

[pt7k]

I believe that 2nd example in the Readme was intended to be as follows:

g[0](y) := 0
g[n](y) := g[n - 1](y)'

Then it's working as described, referencing a prior step instead of itself.

It's also possible to create the same issue in a wff variation, but one must use ! operator in that case, as ' works only with sbf.
So the following will hang the program as well:

g[0](y) := F
g[n](y) := !g[n](y)
n g[5](1)

[pt7k]

It's also possible to run the same example through the interpreter with:
r o1[0] = 0 && o1[n] = o1[n-1]'

But trying to hang it with r o1[0] = 0 && o1[n] = o1[n]' fails, with a proper error message saying that the spec is unsat.

[LEARNTAU]

Hi pk, thanks for your reply.

I agree that Tau should detect this
g[0](y) := 0
g[n](y) := g[n](y)'
n g[5](1)

and give an error message saying this is unsat.

If the formula is satisfiable, then at some time it will give a True statement.
But in this case, it cannot give any True statement at any time t, so it's unsatisfiable.

After changing the second line from g[n](y) := g[n](y)' to g[n](y) := g[n-1](y)'

I normalize it n g[5](1) and Tau gave me a result of 1.

I tried your recommendation from telegram dev chat about running this with an output stream of o1

a[n](x) := g[n](x) <-> o1[n] = 1

then try to normalize again n g[5](1) but it gave me an (Error) Type mismatch. g[1]/1() : wff declared as bf

So if there is only 2 formulas, it normalizes, but adding additional formula, normalize have error.

Now, I tried to run it but gave me Seg fault.

r a[5](1)

here I just tried to make o1[n] = 0 but same thing happens

What I expect is at the 5th step, Tau will give me an answer. Any ideas why?

[pt7k]

Hi @LEARNTAU,
That's not working because you're mixing here the example I gave you for a predicate, and here you have a function (so you are using a formula that expects wff, but is applied to bf). Check again and you will see that you had := T in that definition you were asking about before, that makes it a wff. And here you have := 0, so in this case g is of type bf, hence you have to use a formula that treats g as a bf, for instance a[n](x) := o1[n] = g[n](x)

[LEARNTAU]

Yes, thank you for pointing that out.

<-> is a Tau local spec
T | F is a Tau local spec

0 is a bf term
' is a bf term

Now I got it.