是否有可能在未类型化的lambda演算上有效地实现' max ' ?

Question

min通常在未类型化lambda演算中定义为(使用Caramel的语法):

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，它具有以下属性:

1. a和b在函数体中最多使用一次。

2. 它有一个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是不允许的)，所以我仍然不知道这是否可能。