lambda-calculus

0熱度

1回答

我已經定義教堂數字0，根據維基百科的定義，在教會數字的一些其他的標準功能如下： (define n0 (λ (f x) x)) (define newtrue (λ(m n) m)) (define newfalse (λ(m n) n)) (define iszero (λ(m) (m (λ(x) newfalse) newtrue))) (defi

4熱度

1回答

Unbound是否總是需要在`FreshM` monad中？

我正在使用基於some existing code的項目，該項目使用unbound庫。該代碼使用unsafeUnbind一堆，這是我的問題。我使用freshen試過，但我得到以下錯誤： error "fresh encountered bound name! Please report this as a bug." 我想知道：將是一個FreshM單子內完全使用意庫？還是他們的方式來做

7熱度

1回答

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

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

0熱度

1回答

ANTLR不匹配輸入中的Lambda表達式

我想實現lambda表達式的解析器。但我得到「不匹配輸入'預期 '）'」的錯誤該輸入：（\ XX X）（\ XX X），不知道爲什麼...... 我有一個語法： grammar Lambda; lambda_expression : VARIABLE | '\\' VARIABLE '.' lambda_expression | ('(' lambda_e

0熱度

1回答

lambda微積分上下文中「自由變量」和「變量的自由出現」之間的區別

lambda演算上下文中自由變量和變量自由出現之間是否有區別？如果是的話，請用一兩個例子來解釋。其實我經歷了lambda表達式轉換規則我碰到下面一行哪裏傳來：在說明的轉換規則的符號E[E'/V]用於意味着在V每個自由出現替代E'的結果E

4熱度

1回答

將自然語言轉換成邏輯公式

我試了幾天，寫了一個NLTK語法將簡單的法語句子轉換成邏輯公式。我的問題可能與英語句子類似。我的目標是這個語法接受幾個命令（家庭自動化）並將它們轉換成邏輯公式。訂單的一些例子：打開燈： exists x.(turn_on(x) & light(x)) 打開了綠燈： exists x.(turn_on(x) & light(x) & green(x)) 打開廚房 exists x.(tur

-1熱度

1回答

Y-Combinator definiton

我想了解定點組合器。我認爲它被某些語言用來實現遞歸。主要的問題是，我不能讓下一個定義：所以，請解釋一下形象。

2熱度

1回答

如何在球拍中應用lambda演算規則？

我想測試一下我使用Racket編寫的lambda微積分函數，但沒有太多運氣與測試用例。例如，給定的定義 ; successor function (define my_succ (λ (one) (λ (two) (λ (three) (two ((one two) three)))))) 我試圖將它應用到1 2 3，期望的2的後繼者是3通

2熱度

1回答

圖厄莫爾斯序列在Haskell

的一行我在Haskell的一行寫的Thue-Morse squence定義爲整數的無限名單： thueMorse = 0:1:f (tail thueMorse) where f = (\(x:xs) -> x:(1 - x):f xs) 這是一次失敗的嘗試定義序列的結果在一行中，只有在lambda表達式和它本身方面，沒有let或where表達式（真正應該在兩行上呈現，使得上述解決方案成爲精神

3熱度

4回答

在現代Haskell中可以定義Omega combinator（λx.xx）嗎？

堆棧！在現代Haskell中可以定義Omega combinator（λx.xx）嗎？我猜想，Haskell98的類型系統旨在使這樣的事情變得不可能，但現代擴展又如何呢？