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)