标签: caramel

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. 它具有β正常形式(即,不使用定点组合器强烈正常化).

这样的max定义是否存在？