lambda-calculus

1熱度

1回答

我對lambda微積分很新，在閱讀教程時遇到了這個問題。這是我的等式。 Y = ƛf.(ƛx.f(xx)) (ƛx.f(xx)) 現在，如果我們應用的另一種說法，假設F（YF），那麼我們如何能減少this.If我根據測試減少是正確的，我們可以在替換所有˚F（ƛx .f（xx））由（ƛx.f（xx）），這是正確的，如果是的話，我們該怎麼做。感謝

13熱度

1回答

函數式編程語言中的教會Rosser定理示例

我在學習函數式編程的同時看到了多個對Church Rosser theorem的引用，特別是菱形屬性圖，但我還沒有遇到過很好的代碼示例。如果像Haskell這樣的語言可以被看作是一種lambda演算，那麼它就必須能夠使用語言本身鼓起一些例子。如果示例容易地顯示步驟或減少如何導致容易並行執行，我會給予獎勵積分。

11熱度

1回答

如何找到最佳處理順序？

我有一個有趣的問題，但我不知道如何將其短語... 考慮lambda演算。對於給定的lambda表達式，有幾種可能的縮減順序。但其中一些不會終止，而有些則不會。在λ演算中，事實證明存在一個特定的縮減順序，即保證如果實際存在，總是以不可約的解決方案終止。這叫做正常訂單。我寫了一個簡單的邏輯求解器。但麻煩在於，它處理約束的順序似乎對它是否找到解決方案產生巨大影響。基本上，我想知道我的邏輯編程語言是否

9熱度

1回答

如何使用命名上下文來查找de Bruijn指數的自由變量？

在「類型和編程語言」中，第6.1.2節中他們討論了用於爲lambda表達式中的自由變量編號的命名上下文。使用他們提供的示例方案，λx.xb和λx.xx的de Bruijn表示形式爲λ.00，如果它們有明顯不同的術語。這個怎麼用？

4熱度

2回答

比較語法樹模α-轉化

我工作的編譯器/防爆檢查，我想知道，如果我有一個語法樹像這樣的，例如：如果有辦法檢查Expr的alpha等價（等價模更名）。然而，這個Expr與lambda演算的不同之處在於，λ中的變量集是可交換的 - 即參數的順序不涉及檢查。（爲簡單起見，Lambda ["x","y"] ...不同於Lambda ["x"] (Lambda ["y"] ...)，在這種情況下，順序很重要）。換句話說

1熱度

2回答

一旦在lambda微積分中找到解決方案，將其轉換爲代碼有多容易？

如果您要閱讀一個問題陳述，比如TopCoder上的東西，並將其轉換爲lambda演算表示形式，那麼將此轉換爲Haskell或Lisp代碼是一種簡單的練習嗎？換句話說，使用lambda微積分形式系統可以解決一個問題，然後在函數式編程語言中實現？

20熱度

2回答

什麼是「自由變量」？

（我確定這個網站上已經有這個答案了，但是搜索被C中的一個變量調用free（）的概念所淹沒。）我遇到了「eta還原」這個術語，如果x是「M中不空閒」，則定義爲f x = M x ==> M。我的意思是，我認爲我理解它要說的內容的要點，看起來就像你將一個函數轉換爲無點風格時所做的一樣，但我不知道x是不是免費的限定詞意味着什麼。

5熱度

3回答

一個組合子的類型簽名不匹配等值lambda函數的類型簽名

考慮這個組合子： S (S K) 它應用到的參數XY： S (S K) X Y 它收縮到： X Y 我將S（SK）轉換爲相應的Lambda條款並得到了如下結果： (\x y -> x y) 我用哈斯克爾WinGHCi工具來獲得（\ x和y - > x和y）的類型簽名，它返回： (t1 -> t) -> t1 -> t 這對我來說很有意義。接下來，我用WinGHCi得到S（S

7熱度

3回答

在無類型lambda微積分中嵌入更高kinded類型（monads！）

可以通過高階函數在無類型lambda微積分中編碼各種類型。 Examples: zero = λfx. x one = λfx. fx two = λfx. f(fx) three = λfx. f(f(fx)) etc true = λtf. t false = λtf. f tuple = λxyb. b x y null = λp. p (λxy. false)

5熱度

1回答

隱式參數是GHC內聯的難點嗎？

我很好奇在Functional Pearl: Implicit Configurations文章Kiselyov和撣討論了反對implicit parameters。在存在隱式參數的情況下內聯代碼（β-reduce）並不健全。真的嗎？我希望GHC應該與傳遞的隱式參數一樣嵌入到相同的範圍內，否？我相信我理解他們的反對意見認爲：一個術語的行爲可以改變，如果它的簽名是添加，刪除或更改。 GHC的