是否可以在無類型的lambda演算中有效地實現`max`？

min通常在無類型lambda演算定義爲（使用Caramel's syntax）：是否可以在無類型的lambda演算中有效地實現`max`？

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嗎？

來源

2015-10-06 MaiaVictor

我記得Loic Colson調查過這樣一個問題：系統T，通過價值和最小問題調用，TCS 206,1998。我看了一下，但找不到任何關於max的具體內容。 –

@AndreaAsperti啊原來這個問題並不難，讓我來回答 – MaiaVictor

@AndreaAsperti哦剛剛注意到我問'a'和'b'只能用一次。該死的我和我的要求很高的問題。 – MaiaVictor

從記錄上來看，如果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），所以我仍然不知道這是否可能。

來源

2017-02-04 23:45:17 MaiaVictor

是否可以在無類型的lambda演算中有效地實現`max`？

回答

相關問題