問題タブ [plt-redex]

誰かがリダクションセマンティクスとPLTRedexの使用法をより簡単な言語で説明してください。

ありがとう。

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

私は 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 という言語を定義できます。

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

ドキュメントからの私の理解では、とextend-reduction-relationのルールを再解釈する必要がありますが、lambdaLVar-nats を使用します。これらすべてをまとめて、新しく拡張されたリダクション関係の 1 つを使用して、私が持っていたテスト スイートを実行してみました。slow-rrfast-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 生成マクロを作成するだけで済むのでしょうか?

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

Just starting to learn PLT-Redex... Two questions come up:

1. Can we use PLT-Redex to model side effects? For example: simple increment construct i++?
2. What about thread? All the constructs introduced so far does not involve something like creating an thread? synchronization of the thread? is it doable in PLT-Redex (syntax as well as reduction rule?

Thanks in advance,

言語のセマンティクスを準備しようとしています。一部の派生は、「スタック」状態につながる可能性があります。テストしたいのですが、特定の用語を「スタック」状態に減らすことはできません。のようなものを使用してそれを表現することは何とか可能test-->Eですか?

私は正規の実装を持つ型システムの Redex でモデルを構築することに取り組んでいます。モデルを実際の実装に対してファジング テストするために、redex-check を使用したいと考えています。

実装 (アダプターを使用) は抽象構文を使用できるため、ファザーによって生成された用語を実装に渡す方法が必要です。これを行う方法はありますか？

モデルを別のモデルに対して検証するために redex-check を使用していますが、デバッグ目的で中間 (成功) の結果を確認したいと考えています。これを行う最も明白な方法は、property-expr に与えられた用語を副作用として出力させることですが、これは洗練されていません。中間の redex-check 試行を調べる別の方法はありますか?

次のように、ペアのリストを単一の数値のリストに変換する Redex メタ関数を定義しようとしています。

しかし、 の最後の定義は受け入れられません。すでに 1 つの省略記号の下にあるにも関わらず、Redex は省略記号を必要とし、add-up不平を言っています。Redex の省略記号の各メンバーに Racket unquote を適用する方法はありますか?e_1e_2

次のように、キャストとサブタイプを持つ言語の定義に取り組んでいます。

次に、それに対して次の判断フォームを定義します。

そして今、私の還元関係では、次のようなものを書きたいです

(typeof v)値の型を返すと仮定しますv。私が知る限りwhere-judgment-holds、Redex ライブラリにはそのようなものはありません。引用符を外して回避することはできますが、Redex に何かが組み込まれているとよいでしょう。