plt-redex

4熱

1答えて

私はequi-recursive型とiso-recursive型の両方を非常によく理解していると思います。したがって、私はPLT Redexでequi-recursive型のISWIM用の型チェッカーを実装しようとしていました。しかし、私の人生のために、タイプ同値化の仕方を理解することはできません。他のすべては素晴らしい作品です。これは私の言語である： (define-language iswi

1熱

1答えて

redexで小さな言語を定義しようとしています

私は、Redex用にamb tutorialに従うと同時に、Pierceのタイプとプログラミング言語にある型付き算術式のモデルを構築しています。私はこのような小さな言語の構文と型システムを定義しましたが、小さなステップセマンティクスを定義するのは難しいです。私が問題になる前に、私がこれまでに得た定義を提示しましょう。まず、言語の構文を定義しました。 (define-language ty-ex

0熱

1答えて

PLT-Redexを使用してセマンティクスをテストするときに型付きの言葉のみを生成する

私はラケットには新しく、特にredexの使用に興味があります。私は、Pierceの型とプログラミング言語の本で見つかった型付き算術式の小さなモデルを作成しました。コードは次の要点にあります：https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0 私が進行状況と保存のようなプロパティをテストしようとしたとき、私

2熱

1答えて

Redexで評価コンテキストが必要なのはなぜですか？

評価コンテキストを使用せずに自分の言語の評価ルールを書くことは完全に可能です。私のセマンティクスは完全に価値によって呼び出され、ラムダの中でその言葉が前進していくことを許さない。それにもかかわらず、私が見たすべてのリソースは、何らかの形で還元コンテキストを使用しています。私が紛失している文脈を使う良い理由はありますか？

0熱

1答えて

lisp- "自動車：契約違反が予想される：ペア？:(）"アクセスコントロールモデル内のオブジェクトを破棄中

アクセスコントロールモデル内のオブジェクトを破棄し、すべての状況をシミュレートするプロシージャを作成します。これは私のコードです。 (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)