# Talk:Μ

Jump to navigation
Jump to search

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)