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

Question

min is usually defined on the untyped lambda calculus as (using Caramel's syntax):

sub a b   = (b pred a)
<=  a b   = (is_zero (sub b a))
min a b   = (<= a b a b)

This is terribly inefficient. Sub is quadratic, since it applies pred (which is linear) b times. There is a much more efficient implementation of min as:

min a b 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))

This zips through both numbers in a continuation-passing style until the first zero is reached. Now, I'm trying to find a max that is as efficient as min, that has the following properties:

1. a and b are used at most once on the body of the function.

2. It has a beta normal form (i.e., doesn't use fixed-point combinators is strongly normalizing).

Does such max definition exist?

Answer 1

Just for the records, if a and b can be used twice (i.e., it would involve a dup node on interaction nets), there is a simple solution:

true a b  = a
false a b = b
const a b = a

-- less than or equal
lte a b = (go a true (go b false))
    go  = (num result -> (num (pred cont -> (cont pred)) (const result)))

min  = (a b -> (lte a b a b))
max  = (a b -> (lte a b b a))

-- A simple test
main = (max (max 3 14) (max 2 13))

But I demanded no duplication (i.e., lte a b b a isn't allowed) so I still don't know if that is possible.