PLT Redex：參數化語言定義

這是一個嘮叨我一段時間的問題，我想知道這裏有沒有人可以幫忙。PLT Redex：參數化語言定義

我有一種稱爲lambdaLVar的PLT Redex模型，它或多或少是一種花園式的無類型lambda微積分，但擴展了包含「晶格變量」或LVars的存儲。 LVar是一個變量，其值只能隨着時間增加，其中「增加」的含義由語言用戶指定的部分有序集合（又名格）給出。因此lambdaLVar是一個真正的語言家族 - 用一個格子來實例化它，並且你得到一種語言;用不同的格子，你得到另一個。你可以看看代碼here;重要的東西是在lambdaLVar.rkt。

在lambdaLVar的紙上定義中，語言定義由用戶指定的點陣參數化。很長一段時間裏，我想在Redex模型中做同樣的參數化，但到目前爲止，我還沒有弄清楚如何。部分問題在於語言的語法取決於用戶如何實例化格：格的元素成爲語法中的終端。我不知道如何在Redex中表達一個在格子上是抽象的語法。

與此同時，我試圖使lambdaLVar.rkt儘可能模塊化。該文件中定義的語言專用於特定格：max的自然數作爲最小上界（lub）操作。（或者等價地，按照<=排序的自然數，這是一個非常無聊的格）。特定於該格的代碼的唯一部分是(define lub-op max)靠近頂部，而natural出現在語法中。（有這個在用戶指定的lub-op功能來定義一個lub元函數，後者只是一個球拍的功能，所以lub一直逃避出來球拍調用lub-op。）

除非實際指定lambdaLVar的能力在格子的選擇上是抽象的，似乎我應該能夠編寫一個帶有最基本的格子的lambdaLVar版本 - 只有Bot和Top元素，其中Bot < = Top - 和然後使用define-extended-language添加更多內容。例如，我可以定義專門的土黃語言稱爲lambdaLVar-NATS格老子描述：

;; Grammar for elements of a lattice of natural numbers. 
(define-extended-language lambdaLVar-nats 
    lambdaLVar 
    (StoreVal .... ;; Extend the original language 
      natural)) 

;; All we have to specify is the lub operation; leq is implicitly <= 
(define-metafunction/extension lub lambdaLVar-nats 
    lub-nats : d d -> d 
    [(lub-nats d_1 d_2) ,(max (term d_1) (term d_2))])

然後，更換兩個減速關係slow-rr和fast-rr，我不得不爲lambdaLVar，我可以定義一個夫婦包裝的：

(define nats-slow-rr 
    (extend-reduction-relation slow-rr 
          lambdaLVar-nats)) 

(define nats-fast-rr 
    (extend-reduction-relation fast-rr 
          lambdaLVar-nats))

我從extend-reduction-relation文檔的理解是，它應該重新解釋slow-rr和fast-rr的規則，但使用lambdaLVar-NATS。把這個都在一起，我試圖運行測試套件，我不得不用新的，擴展的減少關係之一：

> (program-test-suite nats-slow-rr)

我得到的第一件事是違反合同的投訴：small-step-base: input (((l 3)) new) at position 1 does not match its contract。小步基的合同行只是#:contract (small-step-base Config Config)，其中Config是一個語法非終結符，如果在lambdaLar-nats下重新解釋，那麼它具有新的含義，因爲它具有特定的晶格內容。作爲一個實驗，我擺脫了small-step-base和small-step-slow的合同。

我當時能夠真正運行我的19個測試程序，但其中有10個失敗。也許不出所料，所有失敗的程序都是以某種方式使用自然數值LVar的程序。（其餘的都是純粹的程序，根本不與LVars存儲進行交互）。所以，失敗的測試恰恰是那些使用擴展語法的測試。

所以我一直跟着兔子洞，似乎Redex希望我擴展所有現有的判斷形式和元功能，以便與lambdaLVar-nats而不是lambdaLVar相關聯。這是有道理的，而且就我所能判斷的判斷形式而言，它似乎仍然可行，但對於元函數，我會遇到麻煩：我想要新的元函數重載同名的舊函數（因爲現有的判斷形式正在使用它），似乎沒有辦法做到這一點。如果我不得不重新命名元功能，它就會失敗，因爲我必須寫出全新的判斷形式。我想我想要的是一種元函數調用的後期綁定！

我一言以蔽之問題：是否有歸約任何方式參數化語言的定義在我想要的方式，或擴展語言定義的方式，將做我想要什麼？我最終會不得不編寫Redex生成的宏？

感謝您的閱讀！

來源

2013-04-03 Lindsey Kuper

我問Racket用戶郵件列表;線程開始here。總結由此產生的討論：在今天的Redex中，答案是no，沒有辦法以我想要的方式參數化語言定義。然而，應可能在未來版本的Redex中使用模塊系統，該模塊系統目前正在開發中。

它也不起作用嘗試使用REDEX現有的擴展形式（define-extended-language，extend-reduction-relation，等等）的方式我想在這裏做，因爲 - 因爲我發現 - 原來元功能沒有得到傳遞性地重新解釋爲使用擴展語言。但是一個模塊系統顯然也會對此有所幫助，因爲它可以讓你將元函數，判斷形式和約簡關係打包在一起，並同時擴展它們（參見討論here）。

因此，現在的答案確實是編寫一個Redex生成宏。像這樣的工作：

(define-syntax-rule (define-lambdaLVar-language name lub-op lattice-values ...) 
    (begin 
    ;; Entire original Redex model goes here, with `natural` replaced with 
    ;; `lattice-values ...`, and instances of `...` replaced with `(... ...)` 
))

然後你就可以實例化，e.g特別格，：

(define-lambdaLVar-language lambdaLVar-nat max natural)

我希望歸約不會很快得到模塊，但在此期間，這似乎運作良好。

來源

2013-04-06 18:58:09

PLT Redex：參數化語言定義

回答

相關問題