plt-redex

2熱度

1回答

我試圖定義一個歸約元函數，它轉換爲對單個號碼的列表清單，如下所享有： #lang racket (require redex) (define-language L (e n ((n n) ...) (n ...)) (n number)) (define-metafunction L ((add-up n) n) ((add-up ((e_1 e

4熱度

1回答

如何在PLT Redex中實現等遞歸類型？

我相信我很好地理解等遞歸類型和iso-recursive類型。因此，我一直試圖在PLT Redex中爲等值遞歸類型實現ISWIM的類型檢查器。但是，對於我的生活，我無法弄清楚如何進行類型對等的工作。其他一切都很好。這是我的語言： (define-language iswim [X ::= variable-not-otherwise-mentioned] [b ::= num

3熱度

1回答

將模型與Redex中的實現進行比較

我正在構建一個類型系統的Redex中的模型，該模型也具有規範的實現。我想用redex-check來模擬測試我的模型與實際的實現。實現（使用適配器）可以使用我的抽象語法，所以我需要的是將模糊器生成的術語傳遞給實現的方式。有沒有辦法做到這一點？

2熱度

1回答

使用redex-check打印成功

我正在使用redex-check來針對另一個模型驗證模型，並希望查看用於調試目的的中間（成功）結果。最明顯的做法是讓屬性表達式將給定的術語打印爲副作用，但這不夠雅觀。是否有另一種方法來查看中間redex-check嘗試？

7熱度

2回答

什麼是「還原語義」？請解釋PLT Redex在外行人員中的使用

有人請以更簡單的語言解釋簡化語義和PLT Redex的用法。謝謝。

12熱度

1回答

PLT Redex：參數化語言定義

這是一個嘮叨我一段時間的問題，我想知道這裏有沒有人可以幫忙。我有一種稱爲lambdaLVar的PLT Redex模型，它或多或少是一種花園式的無類型lambda微積分，但擴展了包含「晶格變量」或LVars的存儲。 LVar是一個變量，其值只能隨着時間增加，其中「增加」的含義由語言用戶指定的部分有序集合（又名格）給出。因此lambdaLVar是一個真正的語言家族 - 用一個格子來實例化它，並且你得

1熱度

1回答

PLT-Redex可以模擬這些功能嗎？

剛剛開始學習PLT-歸約......兩個問題上來：我們可以使用PLT-歸約模型副作用？例如：簡單的增量構造i++？ thread怎麼樣？到目前爲止所介紹的所有構造都不涉及創建線程之類的東西。線程的同步？是可行的PLT-歸約（語法以及減少規則由於提前，

1熱度

1回答

試圖用redex定義一種小語言

我正在關注Redex的amb tutorial，並且同時爲皮爾斯類型和編程語言中的類型化算術表達式構建了一個模型。我已經定義了這種小語言的語法和類型系統，但我很難定義它的小步語義。在我解決問題之前，讓我介紹一下迄今爲止的定義。首先，我定義了語言的語法。 (define-language ty-exp [E (ttrue) (ffalse) (zero)

0熱度

1回答

lisp-「汽車：合同違規期望：對？給定:(）」同時銷燬訪問控制模型中的obj

編寫一個過程以銷燬我的訪問控制模型中的對象並模擬每種情況。這是我的代碼。 (define st1 (term (st 3 2 (,s0 ,s1 ,s2) (,o0 ,o1) ,br ,m1))) (define m1 (term ((,s0 control ,s0) (,s1 (trans ,r1) ,o0) (,s2 ,r2 ,o1)))) (define r1 (term read))

4熱度

1回答

plt-redex：捕獲 - 免費替代？

每次我在PLT redex中定義一種語言時，我需要手動定義一個（捕獲避免）替換函數。例如，這種模式還沒有完成，因爲subst沒有定義： #lang racket/base (require redex/reduction-semantics) (define-language Λ [V ::= x (λ x M)] [M ::= (M M) V] [C ::=