我的Lambda微積分語法明確無誤嗎？

我正在嘗試爲處理lambda微積分的語言編寫一個小型編譯器。這是語言的模棱兩可的定義，我發現：我的Lambda微積分語法明確無誤嗎？

E →^v . E | E E | (E) | v

符號^，（，）和v令牌。 ^表示lambda，v表示變量。形式^ v.E的表達式是一個函數定義，其中v是函數的形式參數，E是它的主體。如果f和g是lambda表達式，那麼lambda表達式fg代表函數f對參數g的應用。

我試圖寫這個語言的明確語法，在假設函數應用程序是關聯的，例如fgh =（fg）h，並且該函數應用程序綁定比。，例如，（^ x ^。ŸXY）^ ZZ =（。^ X（^ŸXY））^ ZZ

這裏是我到目前爲止，但我不知道這是否是正確的：

E -> ^v.E | T 
T -> vF | (E) E 
F -> v | epsilon

有人可以幫忙嗎？

來源

2013-03-02 John Roberts

1）明確的語法不是全部和最終的全部。 – 2013-03-02 04:34:19

2）你爲什麼要用手工來代替使用免費的語法工具，其中許多工具可以在網上免費使用？ – 2013-03-02 04:35:12

小心把我指向一個好的？我對此很新。 – 2013-03-02 05:07:35

在閱讀您的問題和意見之間，您似乎正在尋求更多的幫助，學習和實施lambda演算，而不僅僅是您在此提出的具體問題。如果是這樣，那麼我在同一條路上，所以我會分享一些有用的信息。

我最好的書，這並不是說可能的最好的書，是本傑明C.皮爾斯的Types and Programming Languages（WorldCat）。我知道標題聽起來不像lambda微積分，但看看λ-Calculus extensions: meaning of extension symbols，其中列出了許多來自該書的lambda結石。這本書的代碼是OCaml和F#。

嘗試在CiteSeerX中搜索有關lambda微積分的研究論文以瞭解更多信息。

最好的λ演算評估到目前爲止，我所發現的是：

Lambda calculus reduction workbench與信息here。

此外，我發現你可以得到更好的答案，在編程和數學相關的問題Math:StackExcahnge有關的lambda微積分問題。

至於編程語言來實現lambda微積分，如果你還沒有學習，你可能需要學習一個functional language;是的，這是一個不同的野獸，但在山的另一邊的啓蒙是壯觀的。我發現的大多數源代碼都使用ML或OCaml等功能語言，一旦你學習了一個，其餘的就會更容易學習。

更具體地講，here是無類型演算項目的源代碼，here是輸入文件YACC的F＃的變化，這從閱讀你以前questions似乎是在你的知識世界，here是樣本輸入。

由於語法是用於實現REPL，它始於頂層，思考命令提示符，並接受多個命令，在這種情況下是lambda演算表達式。由於這個語法被用於許多結石，它在前面的例子中有部分是佔位符，因此這裏的綁定更像是一個佔位符。

最後，我們得到了一部分，你是後

注意LCID是小寫字母標識符

Term : AppTerm 
    | LAMBDA LCID DOT Term 
    | LAMBDA USCORE DOT Term 

AppTerm : ATerm 
     | AppTerm ATerm 

/* Atomic terms are ones that never require extra parentheses */ 
ATerm : LPAREN Term RPAREN 
     | LCID

來源

2013-03-02 06:41:26

感謝您的回答。 USCORE術語在你提供的語法中有點困惑 - 這似乎不屬於我上面指定的語言的一部分。另外，你提供的語法似乎是左遞歸的，這是我目前試圖避免的。你能否評論我寫的語法的有效性？ – 2013-03-02 16:11:18

@JohnRoberts在回答之前，我需要更多地關注USCORE，我使用項目中的其他一些語法。正如Pieter Geerkens所說，不要掛在語法上。很久以前，我做了同樣的事情，現在我在AST上進行嘗試，並使用許多解析器之一，即LL，LR，解析器combinatros，手動構建遞歸下降等來創建AST。爲了確定你的語法是否可怕，你需要指定它們的解析器類型。這個語法是針對一個LR paser，但你似乎在LL語法之後，不是？ – 2013-03-02 16:49:15

我正在尋找一個LALR（1）解析器語法 - 我只是首先檢查LL（1）作爲快速驗證。再看看我的語法，在我看來，它無法處理字符串末尾的括號表達式的情況，例如λx.λy.λz.x（y z） - 您是否也看到了這一點？ – 2013-03-02 16:56:10

您可能會發現在次線性時間特定語法的模糊性的證明，但證明的語法是明確的是一個NP完整的問題。你必須用語言生成每一個可能的句子，並檢查每個句子只有一個派生。

來源

2013-03-03 00:43:36 Apalala

我的Lambda微積分語法明確無誤嗎？

回答

相關問題