Is it possible to effectively implement `max` on untyped lambda calculus?

Question

min usually defined on an untyped lambda calculus as (using caramel syntax ):

 sub ab = (b pred a) <= ab = (is_zero (sub ba)) min ab = (<= abab) 

This is terribly inefficient. Sub is quadratic because pred (which is linear) is applied b times. There is a much more efficient min implementation like:

 min ab succ zero = (a a_succ (const zero) (b b_succ (const zero)))) a_succ pred cont = (cont pred) b_succ pred cont = (succ (cont pred)) 

It fastens on both numbers in a continuation style until the first zero is reached. Now I am trying to find max , which is as efficient as min , which has the following properties:

• a and b are used no more than once in the function body.

• It has a beta-normal form (i.e., it does not use fixed-point combinators, is very normal).

Is there such a definition for max ?

Answer 1

For records only, if a and b can be used twice (i.e. it will include a dup node in interaction networks), there is a simple solution:

 true ab = a false ab = b const ab = a -- less than or equal lte ab = (go a true (go b false)) go = (num result -> (num (pred cont -> (cont pred)) (const result))) min = (ab -> (lte abab)) max = (ab -> (lte abba)) -- A simple test main = (max (max 3 14) (max 2 13)) 

But I did not require duplication (i.e. lte abba not allowed), so I still don't know if this is possible.