是否可以在无类型的 lambda 演算上有效地实现“max”？答案

【问题标题】：Is it possible to implement `max` efficiently on the untyped lambda calculus?是否可以在无类型的 lambda 演算上有效地实现“max”？
【发布时间】：2015-10-06 12:52:08
【问题描述】：

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

这会以连续传递的方式遍历两个数字，直到到达第一个零。现在，我正在尝试找到一个与min 一样高效的max，它具有以下属性：

a 和 b 在函数体中最多使用一次。
它具有 beta 范式（即，不使用定点组合器是强归一化的）。

这样的max定义存在吗？

【问题讨论】：

我记得 Loic Colson 研究过这类问题：System T, call by value and the minimum problem, TCS 206, 1998。我看了看，但找不到关于 max 的任何具体信息。
@AndreaAsperti 啊原来问题不那么难，让我来回答吧
@AndreaAsperti 哦，刚刚注意到我要求a 和b 只使用一次。该死的我和我的苛刻问题。

标签： functional-programming lambda-calculus caramel

【解决方案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 是不允许的）所以我仍然不知道这是否可能。

【讨论】：