# 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

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)