13

これは私がしばらく悩まされてきた問題であり、ここにいる誰かが助けてくれるのではないかと思います.

私は lambdaLVar と呼ばれる言語の PLT Redex モデルを持っています。これは、多かれ少なかれさまざまな型付けされていないラムダ計算ですが、「格子変数」または LVars を含むストアで拡張されています。LVar は、時間の経過とともに値が増加する変数です。「増加」の意味は、言語のユーザーが指定する部分的に順序付けられたセット (ラティスとも呼ばれます) によって与えられます。したがって、lambdaLVar は実際には言語のファミリーです。1 つのラティスでインスタンス化すると、1 つの言語が得られます。別のラティスを使用すると、別のラティスが得られます。ここでコードを見ることができます。重要なものはlambdaLVar.rktにあります。

lambdaLVar の紙上の定義では、言語定義はユーザー指定のラティスによってパラメーター化されます。長い間、Redex モデルで同じ種類のパラメーター化を行いたいと思っていましたが、これまでのところ、その方法を理解できていません。問題の一部は、言語の文法がユーザーがラティスをインスタンス化する方法に依存することです。ラティスの要素は文法の端子になります。ラティス上で抽象的な文法を Redex で表現する方法がわかりません。

その間、lambdaLVar.rkt をできるだけモジュール化しようとしました。そのファイルで定義されている言語は、特定のラティスに特化されています。つまりmax、最小上限 (lub) 操作としての自然数です。(または、同じように、自然数は によって並べられ<=ます。これは非常に退屈なラティスです。) そのラティスに固有のコードの部分は(define lub-op max)、上部近くの行でありnatural、文法に表示されます。(lubユーザー指定の関数に関して定義されたメタ関数がありlub-opます。後者は単なる Racket 関数であるため、Racketlubにエスケープして を呼び出す必要がありますlub-op。)

lambdaLVar をラティスの選択よりも抽象的な方法で実際に指定する機能を除けば、ラティスの最も必要最小限の要素 (Bot 要素と Top 要素のみ) を使用して lambdaLVar のバージョンを記述できるようにする必要があるように思われます。 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))])

次に、 lambdaLVarの 2 つのリダクション関係を置き換えるためにslow-rr、いくつかのラッパーを定義できます。fast-rr

(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のルールを再解釈する必要がありますが、lambdaLVar-nats を使用します。これらすべてをまとめて、新しく拡張されたリダクション関係の 1 つを使用して、私が持っていたテスト スイートを実行してみました。slow-rrfast-rr

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

最初に受け取ったのは、契約違反の苦情です: small-step-base: input (((l 3)) new) at position 1 does not match its contract. small-step-base のコントラクト ラインは just#:contract (small-step-base Config Config)です。ここで、Configは lambdaLVar-nats の下で再解釈した場合に、lambdaLVar の下で行ったよりも新しい意味を持つ文法の非終端記号です。small-step-base実験として、とのコントラクトを削除しましたsmall-step-slow。

その後、実際に 19 個のテスト プログラムを実行できましたが、そのうちの 10 個は失敗しました。当然のことかもしれませんが、失敗するのはすべて、何らかの方法で自然数の値を持つ LVar を使用するプログラムです。(残りは、LVar のストアとまったく対話しない「純粋な」プログラムです。) したがって、失敗するテストは、まさに拡張文法を使用するものです。

そこで、私はうさぎの穴をたどり続けました。Redex は、既存のすべての判断フォームとメタ関数を、lambdaLVar ではなく lambdaLVar-nats に関連付けるように拡張することを望んでいるようです。それは理にかなっており、私が知る限り、判断フォームでは問題ないように見えますが、メタ関数では問題が発生します。新しいメタ関数で同じ名前の古いメタ関数をオーバーロードしたい (既存の判断フォームがそれを使用しているため) ）そして、それを行う方法はないようです。メタ関数の名前を変更しなければならない場合、それは目的を無効にします。とにかく、まったく新しい判断フォームを作成する必要があるからです。私が望むのは、一種のメタ関数呼び出しの遅延バインディングだと思います!

一言で言えば、私の質問: Redex で、言語の定義を希望どおりにパラメータ化する方法、または言語の定義を希望どおりに拡張する方法はありますか? Redex 生成マクロを作成するだけで済むのでしょうか?

読んでくれてありがとう！

4

1 に答える 1

5

Racket ユーザーのメーリング リストに質問しました。スレッドはここから始まります。結果として得られた議論を要約すると: 今日の Redex では、答えはノーです。私が望む方法で言語定義をパラメーター化する方法はありません。ただし、現在作業中のモジュールシステムを備えた Redex の将来のバージョンでは可能になるはずです。

また、ここでやろうとした方法で Redex の既存の拡張形式 ( define-extended-language、extend-reduction-relationなど) を使用しようとしてもうまくいきません。言語。しかし、モジュール システムは明らかにこれにも役立ちます。なぜなら、メタ関数、判断形式、還元関係を一緒にパッケージ化し、同時にそれらを拡張できるからです (ここでの議論を参照してください)。

したがって、現時点での答えは、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 `(... ...)`
))

次に、特定のラティスをインスタンス化できます。たとえば、次のようにします。

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

Redex がすぐにモジュールを入手できることを願っていますが、当面はこれでうまくいくようです。

于 2013-04-06T18:58:09.713 に答える