Lambda微積分表達式測試臺？

我想測試一下Lambda微積分解釋器，我已經寫了一個相當大的Lambda微積分表達式測試集。有誰知道我可以使用的Lambda Calc表達式生成器（在Google上進行初始搜索時找不到任何內容）？這些表達式顯然必須適當形成。更好的是，儘管我自己創建了各種示例並制定瞭解決方案，以便檢查結果，但是有誰知道一個好的（和很大的）一套解決Lambda Calculus減少問題的方法嗎？我可以自己輸入表達式，所以更重要的是隻要有一些簡單的（和更大的）lambda微積分表達式，我可以測試我的解釋器（目前模擬正常順序和按名稱調用評估策略）。Lambda微積分表達式測試臺？

任何幫助或指導將不勝感激。

來源

2013-03-28 9codeMan9

這有幫助嗎？ http://stackoverflow.com/a/15171626/1243762和http://cs.stackexchange.com/questions/9001/test-cases-for-calculus –

是的，這確實很重要。謝謝！ – 9codeMan9

您是否閱讀過[聊天]（http://chat.stackoverflow.com/rooms/25426/lambda-calculus）？ –

Asperti和圭里尼（1998年，函數式編程語言，銀聯新聞的最佳實現;尤其見第5,6章）介紹一些從redexes家庭的讓 - 雅克·利維的理論出現的更痛苦的lambda項的並標記爲減少：這些措施衡量了相互作用的複雜性，這些相互作用是在相互影響的β值降低之間進行的，在這種情況下，redex可以爲另一個創建工作。

碰撞減少的一個相對簡單的例子是：

let D = λx(x x); F= λf.(f (f y)); and I= λx.x in 
    (D (F I))

其中有兩個β-redexes，並減少了(y y)：減少它們中的一個定期替換和您將創建兩個新的redexes，每個與原始術語中的一個結構有關。

迭代Church數是在以相同的方式好：

let T = λfx. f(f(x)) in 
    λfx.(T (T (T (T T))) f x)

（這減少了65 536教會標記），在生成大量碰撞redexes的。

通常，相互應用更高階的術語，無論它們是「良好類型的」還是明顯的意義，都是生成複雜中間結構的努力工作的良好來源。

來源

2013-05-02 07:44:23

你的第二個例子是錯誤的。它應該評估教會的數字爲65536. – mk12

@ mk12：確實如此。我會解決我的答案。 –

Lambda微積分表達式測試臺？

回答

相關問題