functional-programming - 是否可以在无类型 lambda 演算上有效地实现 `max`？

Question

min通常在无类型 lambda 演算上定义为(使用 Caramel's syntax ):

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

这是非常低效的。 Sub是二次的，因为它适用 pred (这是线性的) b次。 min 有一个更有效的实现作为:

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))

这以连续传递的方式通过两个数字，直到达到第一个零。现在，我试图找到一个 max这与 min 一样有效，具有以下性质:

a和 b在函数体上最多使用一次。

它有一个 beta 范式(即，不使用定点组合器是强归一化的)。

是否这样 max定义存在吗？

Answer 1

仅供记录，如果 a和 b可以使用两次(即，它将涉及交互网络上的 dup 节点)，有一个简单的解决方案:

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))

但我要求不重复(即不允许 lte a b b a)，所以我仍然不知道这是否可能。