Talk:μ

For the evaluation of recursive functions to terminate, there has to be some short-circuit mechanism.

• a <= b can short-circuit to 1 if a is zero
• a <= (b <= c) can short-circuit to 0 if a is greater than one

Here is an ugly definition of + that terminates:

 (+) a b c = (not ((a == zero) && (b <= c))) <= (inc (a == zero) <= (one <= ((dec a + inc b) <= c)))

Here is a shorter definition of one:

 one a = a

--Qpliu (talk) 23:40, 18 April 2021 (UTC)

Are you sure that a <= (b <= c) short-circuiting to 1 if a is zero is necessary?

I think the following definition of (<=) is enough:

(<=) :: Nat -> Nat -> Nat
Zero <= _ = Succ Zero
(Succ a) <= (Succ b) = a <= b
_ <= _ = Zero

See the implementation at https://github.com/Hakerh400/haskell-projects/tree/master/mu

It seems that the current definition of (+) properly terminates for all inputs (although it has exponential time complexity). --Hakerh400 (talk) 08:19, 19 April 2021 (UTC)

I now see that I was inadvertently evaluating function arguments strictly, causing infinite recursion (as well as the evaluation of dec zero) in the second argument of ->, which I misinterpreted as being due to a non short-circuiting expression. --Qpliu (talk) 17:21, 19 April 2021 (UTC)

turing completeness?

I dont see any way to loop, and as such not any way to be Turing complete. Additionally, there is not proof. Could we perhaps get one? --Yayimhere2(school) (talk) 20:07, 24 January 2026 (UTC)

Recursion is used in the addition example, so that works as a method of looping. The μ operator itself can also be used for looping, though I'm not sure how applicable that is here (I haven't actually tried making anything in the language). –PkmnQ (talk) 03:16, 25 January 2026 (UTC)

It would be nice to see µ actually defined --Yayimhere2(school) (talk) 14:55, 26 January 2026 (UTC)