日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

拡張性の高い遷移系を記述可能な領域特化言語
馬谷 誠二

遷移系は，言語処理系やモデル検査器など様々なソフトウェアシステムの中核と言える．小規模な遷移系の形式的定
義は，記述・読解・保守等を比較的容易に行うことが可能であるが，一般に，現実世界のシステムに内包されている遷移系は大規模であることが多い．そのため，遷移系記述の拡張性や実行効率を向上させることが重要である．本論
文では，実用的なシステムに埋め込むのに十分な実行効率と拡張性を備えた遷移系を，簡潔に記述可能な領域特化言語（DSL）について提案する．まず，一連のプログラミング言語群の操作的意味論を我々の DSL を使って段階的に定義することにより，その拡張性を例示する．さらに，先行研究の一つである Redex との性能比較を行い，我々のDSL が実行時間で大幅な改善を達成できていることを示す．

いていない．まず，記述の簡略化を優先するが故に，

1 はじめに記述された遷移系の実行速度を犠牲にしがちである．

遷移系（transition system）は，様々なコンピュー

例えば，Redex で記述された Racket のマクロシス

タシステムの動作モデルを簡潔に記述するために広テムの実行モデル [4] は，対象となるベンチマークプ

く用いられている．例えば，プログラミング言語処理

ログラムのサイズが少しでも大きくなると，実行時間

系の構文解析や意味解析，プログラム検証，モデル検が大幅に増大する．また，既存のツールで記述された

査，ネットワークプロトコルの実装など，多くのシス遷移規則は，その再利用性や拡張性が限定的である．

テムやライブラリに内在している．

再利用性が不十分であると，同じ遷移規則を重複して可読性と保守性の観点から，遷移系は可能な限りそ記述する必要が生じる．例えば，実世界のアプリケーの仕様に近い形で記述されるのが望ましい．いくつかション開発においては，わずかに異なるいくつかのバの既存ツール [8] [9] [11] では，遷移系の実行可能な仕リエーション（例えば，ネットワークプロトコルの複様を記述する方法を提供している．Redex [8] は，S数のバージョン）を含む，複数の遷移系を段階的に開式で表現された項に対する強力なパターンマッチ機能

発することがあり得る．あるいは，プログラミング言を提供している．それによって，複雑な内部構造を持語の意味解析フレームワークにおいては，推論したい

つ状態間の遷移規則（transition rule）を，形式的な性質に応じて，微妙に性質の異なる複数の遷移系を同定義と同程度に簡潔かつ理解しやすい形で記述するこ

時に使用することも考えられる．

とを可能にしている．典型的な応用例として，プログ

一般に，遷移規則の記述において，効率性と柔軟

ラミング言語の非決定的操作意味論に基づく抽象解釈

性はトレードオフの関係にある．我々は，実システム（意味解析手法の一種）の実装 [7] などが挙げられる．

に組み込むことを目的とした遷移系を記述するため

しかしながら，既存のツールにはいくつかの問題に，拡張性と効率性の両方の利点を備えた遷移系を記があり，より大規模で実用的な遷移系の構築には向述可能な領域特化言語である LwRed（LightWeighta DSL for Describing Extensible Transition Systems.
Seiji Umatani, 神奈川大学情報学部, Faculty of Informatics, Kanagawa University.

REDucer）を提案する．実際にいくつかの性能評価を行うことにより，LwRed が既存のツールに比べ実行速度を大幅に向上していることを示す．一方，LwRed

は柔軟性を少し犠牲にして設計されているが，ホスユニットである．reducer-of は，簡約関係を表すユト言語 Racket [6] の表現力を上手く活用することで，ニットから（パラメータ化された）遷移関数を取り出実行速度を犠牲にすることなく，実用上，ほとんどのす．また上のコードは該当しないが，簡約関係は任意

規則を簡潔に記述することを可能にしている．これに個の識別子をパラメータとして抽象化することも可能

ついても，いくつかの例を用いて詳しく説明する．

である（2. 4 節参照）．パラメータ化されていない簡

本 論 文 の 構 成 は 次 の と お り で あ る ．2 節 で は ，約関係を使う場合には，その遷移関数を無引数で呼び

LwRed の設計および特徴について説明する．3 節

出すことによりインスタンス化しなければならない．

では，LwRed が Racket の埋め込み DSL としてど

apply-reduction-relation*を用いると，複数スのように実装されているかを詳しく説明し，4 節ではテップの遷移を繰り返し，遷移不可能な状態（つまその性能を先行研究ツールと比較する．5 節では関連

り，どの遷移規則にもマッチしない状態）の集合を研究について触れ，最後に 6 節で結論を述べる．

得られる．例えば，次の簡約関係-->1-red は，入力

cons セルの car 部または cdr 部を非決定的に抽出し，

2 設計

すべてのアトミックな要素の集合 {1, 2, 3} を返す．

本節では，LwRed が提供する機能について，純粋(define-reduction -->1-red

型なしラムダ計算 [1] の拡張である PCF 言語 [10] の[(cons x y) x "car"]

簡約関係を段階的に構築するプロセスを示すことにより説明する．

[(cons x y) y "cdr"])(define -->1 ((reducer-of -->1-red)))(apply-reduction-relation* -->1

2. 1 基本機能
遷移規則の集合（簡約関係と呼ぶことにする）は，
次の define-reduction 構文によって定義される：(define-reduction reduction-name[pattern body ... rule-name] ...)
各節は Racket の match構文とほぼ同じである．実際，

pattern には任意の matchパターンを指定できる．各節の末尾にある rule-name は，簡約関係を拡張する
際，上書き対象を指定するために用いられる（2. 2 節参照）．例えば：(define-reduction -->0-red[(cons x y) x "car"])は簡約関係-->0-red を定義しており，cons セルを状態として受け取り，その car 部を 1 ステップの簡約を行った後の状態として返す．

define-reduction によって定義された簡約関係
から，State → P(State) の遷移関数（transfer func-tion）を取り出すには，次のようにする：(define -->0-gen (reducer-of -->0-red))(define -->0 (-->0-gen))(-->0 (cons 1 2)) ; ⇒ (set 1)
簡約関係は Racket ユニットシステムにおける 1(cons (cons 1 2) 3)) ; ⇒ (set 1 2 3)
ここまでに説明した LwRed の機能を用いて，型なし純粋 λ 計算（LAM） [1] の簡約関係を定義してみる．構文は以下のとおり:

e ::= x | (λ (x) e) | (e e)ただし，変数 x は Racket のシンボルで表現することにする．唯一の簡約規則は次のように定義される：((λ (x) e1 ) e2 ) −→β e1 [e2 /x]
ここで e1 [e2 /x] は代入を表し，Racket による標準的な定義は次のとおり：(define (subst e x e*) ; : e x e → e(match e[(? symbol? y) (if (eq? x y) e* e)][`(λ (,(? symbol? y)) ,e1)(if (eq? x y)`(λ (,y) ,e1)(let ([y-new (gensym y)])`(λ (,y-new),(subst (subst e1 y y-new)x e*))))][`(,e1 ,e2) `(,(subst e1 x e*),(subst e2 x e*))]))
ここでは gensym を素朴に用いることで，名前の誤った補足を回避している．subst を用い，β 規則は次の由な順序で書くことができる．

ように単純に定義できる：(define-reduction -->LAM-red[`((λ (,x) ,e1) ,e2)
(subst e1 x e2) "β"])2. 2 文脈パターン#:with構文と一緒に用いるもう一つの代入演算子<-を用いると，値の集合へと評価される式をその右次に，LAM を拡張して，以下の構文を持つ PCF

辺に書くことができ，左辺に書かれた変数は非決定的言語 [10] に対する簡約関係を定義してみる（簡約規にその集合の要素の一つに束縛される．この束縛演算

則の数学的定義は省略する）．
e ::= · · · | n | (+ e e) | (<= e e)

| (if e e e) | (fix e)
LwRed では，オブジェクト指向言語におけるク子と非決定的モナド [12] に値の集合を注入する liftを用いることで，例えばある簡約を別に定義された簡約の中に埋め込むことができる．

ラスメンバの継承のように既存の簡約関係にいくつこれを用いることで，評価文脈（evaluation con-かの規則を追加することにより，新しい簡約関係をtext）の記述が可能となる．例えば，前節の PCF0 で定義できる．親の簡約関係から規則を継承するには，は (if (<= 10 8) 3 2) のような項は簡約できない

define-reduction の#:superキーワードで親の名前を指定する †1 ．

が，上記の束縛演算子を用いると，条件式における評(define-reduction -->PCF0-red(define-reduction -->PCF1-red

価文脈を PCF0 に追加できる：#:super -->LAM-red[`(if ,e1 ,e2 ,e3)[`(+ ,(? num? n1) ,(? num? n2))#:with e1* <- (lift (-->PCF0 e1))(+ n1 n2) "+"]`(if ,e1* ,e2 ,e3) "ECif"])[`(<= ,(? num? n1) ,(? num? n2))(define -->PCF1 ((reducer-of -->PCF1-red)))#:with n := (<= n1 n2)(apply-reduction-relation* -->PCF1

n "le"]'(if (<= 10 8) 3 2))[`(if #f ,e2 ,e3) e3 "if-false"]

e1 の遷移結果を埋め込むことにより，条件節の簡約[`(if ,e1 ,e2 ,e3)を実現できている．

#:when (not (false? e1))

しかしながら，(if (if (<= 10 8) 3 2) ...) の

e2 "if-true"]

ような入れ子の評価文脈はまだ表現できていない．

[`(fix (λ (,x) ,e))

PCF0 から継承した簡約関係を，規則の一部に自分自#:with y := (gensym 'y)

身による遷移を埋め込むよう定義することにより，評`((λ (,x) ,e)(λ (,y) ((fix (λ (,x) ,e)) ,y)))"fix"])(define -->PCF0 ((reducer-of -->PCF0-red)))
上のいくつかの規則の本体では，#:whenと#:withが使われているが，これらは通常の Racket の構文ではない．
「#:when e」はパターンマッチの追加の条件を

価文脈の再帰的構造を表現することができる．そのよ
うにして，さらに条件式以外の評価文脈も加えると，次の定義が得られる †2 ：(define (val? x)(match x[(? num?)#t][(? boolean?) #t]

指定しており，e が#f と評価された場合，当該規則[`(λ (,x) ,e) #t]

はマッチしないものとみなされる．
「#:with x := e」

[_

#f]))

は，Racket の let構文同様，新しい変数束縛を導入
する．1 つの規則中に任意個の#:when，#:withを自†1 num?は number?の別名である．以降，特に断わることなく同様の別名を使用することにする．

†2 本論文では，「....」はコードの省略の意味で使われ，「...」は構文パターン／テンプレートにおける繰り返しを意味する．

(define-reduction -->PCF2-red(cxt EC (? val? v) `(if □ ,p1 ,p2))#:super -->PCF0-red=⇒ ; expands to[`((λ (,x) ,e) ,(? val? v)) ; override(and `(if ,(? val? v) ,_ ,_)(subst e x v) "β"](app (match-lambda[`(if ,e1 ,e2 ,e3) ; override[`(if ,_ ,p1 ,p2)(λ (e) `(if ,e ,p1* ,p2*))])#:when (and (val? e1) (not (false? e1)))e2 "if-true"]EC))[`(,e1 ,e2)

ホールにフィットする項は，述語 val?によって値だ#:with e1* <- (lift (-->PCF2 e1))

けに限定されている．また，matchの andパターンと`(,e1* ,e2) "EC-app1"]

app パターンを組み合わせることにより，再構築関数....

EC を構成することができる．ここで，p1*と p2*は，[`(if ,e1 ,e2 ,e3)#:with e1* <- (lift (-->PCF2 e1))`(if ,e1* ,e2 ,e3) "EC-if"][`(fix ,e)#:with e* <- (lift (-->PCF2 e))`(fix ,e*) "EC-fix"])(define -->PCF2 ((reducer-of -->PCF2-red)))"β"規則と"if-true"規則を上書きして，値呼びの評
価戦略に従うようにしている．
上記の定義では，遷移する可能性のあるすべての部

ユーザの記述した（複雑かも知れない）パターン p1と p2 から変数束縛のためだけに導出されたパターン
である．

cxt の助けを借りることにより，PCF の値呼び評
価文脈 EC を次のように定義できる：(define-match-expander EC(syntax-parser[(EC p)#'(cxt EC p`(fix □)

分項に対し，それぞれの評価文脈を指定するという類`(+ ,(? val? v) □)似した規則が繰り返されており，冗長なコードとなっ`(+ □ ,e1)ている．LwRed が Racket 標準の matchを利用して`(<= ,(? val? v) □)いることを上手く用いることにより，この冗長性を排`(<= □ ,e1)除することができる．具体的には，以下の説明のよう`(if □ ,e1 ,e2)に define-match-expanderを使ってユーザ定義の文`(,(? val? v) □)脈パターンを定義する．

`(□ ,e1))]))

まず，簡単な例を使って，補助的なパターンエク

例えば，次の式：

スパンダ (cxt C p c ...) について説明する．cxt(match '(if (+ 1 2) (* 3 4) 5)の完全な定義は付録 A に載せている．
「c ...」とい[(EC e) (EC `(<= ,e ,e))])うフォームの列は，パターン中の複数の可能な文脈フォームを意味する．それぞれの文脈フォームは，ホールを表す特別なシンボル□を一つだけ含んでいる．これら複数の文脈フォームは，matchの単一の orパターンに展開される．識別子 C は，このパターンにマッチする文脈を再構築する関数に束縛される．パ
ターン p はホールに埋め込まれるパターンを指定すは (if (<= (+ 1 2) (+ 1 2)) (* 3 4) 5) へと評価される．
最終的に，評価文脈をサポートする PCF3 は，ECを用いて次のように定義することができる：(define-reduction -->PCF3-red#:super -->PCF0-red[`((λ (,x) ,e) ,(? val? v))(subst e x v) "β"]る．例えば，if式の条件節に対する文脈だけからな[`(if ,e1 ,e2 ,e3)

る単純な評価文脈を表現する cxt パターンとその展#:when (and (val? e1) (not (false? e1)))

開後パターンは次の通りである．

e2 "if-true"][(EC e)(define (f x) `(+ ,x 1))#:with e* <- (lift (-->PCF3 e))(define-reduction -->2-red(EC e*) "EC"])[`(f ,x) (f x) "f"])様々な種類の評価文脈中の遷移を単一の"EC"規則にの下，(((reducer-of -->2-red)) '(f a)) は'(+ a 1)

まとめることにより，コード量を削減できている．さとなるが，異なるスコープ中（例えば，異なるモジュー

らに，"EC"規則だけを上書きすることで他の評価戦ル中）で：略に切り替えることも簡単にできる．何より，EC を(define (f x) `(* ,x ,x))使って書かれたコードは，それに対応する形式的な定(define-reduction -->3-red

義に近く，読みやすくコンパクトである．

#:super -->2-red)と定義すれば，規則"f"中の変数参照 f は新しい定義を

2. 3 レキシカル・スコープからの逸脱
前節の PCF3 は，LAM 用の subst 関数の定義を参照しているため不完全である．例えば：(->PCF3 '((λ (x) (+ x 1)) 2))指すことになり，(((reducer-of -->3-red)) '(f a))は'(* a a) となる．
上記のスコープ規則に従って subst 関数を再定義した PCF の定義は次のとおり：

は，式 (+ x 1) に対する代入が未定義なため失敗;; subst for PCFする．

(define (subst e x e*) (match e ...))

PCF 用の subst 関数を再定義することは必要だが，それに加え，親簡約関係（つまり LAM）中の規則に(define-reduction -->PCF4-red#:super -->PCF3-red[(EC e)含まれるすべての subst 関数への参照を置き換える#:with e* <- (lift (-->PCF4 e))

必要がある．subst 関数を参照しているすべての規(EC e*) "EC"])

則を一つ一つ単純に上書きすれば問題は解決するが，自分自身による簡約（つまり-->PCF4）を参照する必

それでは継承の利点が損われてしまう．一方，形式的要があるため，"EC"規則だけは上書きする必要があ

な記述，特にプログラミング言語の意味論の形式的なるが，それ以外の全ての規則は継承によって再利用で定義においては，言語を拡張する際，付随する補助定

きる．

義も暗黙のうちに拡張され，既存の規則中に含まれる

実 際 の LwRed で は ，メ タ 関 数 を 定 義 す る た

同名の定義への参照は自動的にリダイレクトされる

め の 専 用 の define-metafunction フォー ム を 使と仮定されることが多い．今回，新しい定義を自動的

用 し て subst 関 数 を 定 義 す る こ と も で き る ．

かつ暗黙のうちに生成することは我々のツールの目的

define-metafunction では，define-reduction とではないが，既存の参照を新しく書かれた定義にリダ

同様に，継承，上書き，レキシカル・スコープ規則かイレクトする機能は，自然な記述のために不可欠であらの逸脱を利用でき，親メタ関数との差分だけを記述ると言える．

することで新しい定義を書くことができる．

そこで，LwRed の define-reduction は，通常のRacket のレキシカル・スコープ規則とは異なるスコー

2. 4 パラメータ化された簡約

プ規則に従うことにする．具体的には，親簡約関係か簡約関係定義を取り巻く文脈が，定義中で同時にら継承されたすべての規則は，あたかも子簡約関係使用される識別子の集合を成している場合，2. 3 節のの中に「字面上」埋め込まれているかのように振る舞

レキシカル・スコープからの逸脱を用いることがでうことにする（コード量が増大してしまうため，実装

きる．しかしながら，（例えば:=と<-のように）切りで本当に埋め込んだりはしていない．詳細は 3. 4 節

替えたい複数の名前が文脈中に同時に見えており，か参照）．

つ，それぞれが異なる名前を持っている場合，それら簡単な例として，以下の定義：を切り替えながら使用することはできない．そのような場合のため，LwRed は，識別子の列 param ...でパラメータ化された簡約関係を定義する次の形式を

定義を変更する：(define select lift)

提供している：次に，:=<1>は:=のまま，:=<2>を<-でインスタンス(define-reduction (reduction-name param ...)

化する：

...)

(define-reduction

パラメータ化された簡約関係の例として，非決定的(-->PCF6-red --> :=<1> :=<2>)

な選択構文 amb を PCF に追加してみる．まず，amb#:super (-->PCF5-red --> :=<1> :=<2>))

は確率的に選択を行うという規則を含んだベース言(define -->PCF6* (reducer-of -->PCF6-red))

語-->PCF5 を定義する：(define -->PCF6 (-->PCF6* -->PCF6* := <-))

(define select random-ref)(define-reduction(-->PCF5-red --> :=<1> :=<2>)(apply-reduction-relation* -->PCF6 e5); ⇒ {32 33 34 21 22 ... 31 11 43 12 44}
パラメータ-->を子簡約関係-->PCF6*にすることで，[`(<= ,(? num? n1) ,(? num? n2))‌"EC"規則を含む全ての親簡約規則をそのまま再利用#:with n :=<1> (<= n1 n2)

できている．

n "le"]....

2. 5 ユニットシステムとの統合[`(amb ,es ...)

最後に，LwRed の拡張性を向上させるもう一つの#:with e* :=<2> (select es)
e* "amb"]

機能を紹介する．
レキシカル・スコープからの逸脱により，親簡約関[(EC e)#:with e* <- (lift((--> --> :=<1> :=<2>) e))(EC e*) "EC"])

係中からの名前の参照が，子簡約関係の定義を囲む
コードで定義されている名前を参照できるようになる．しかし，大規模なソフトウェア開発においては，

こ れ ま で の:=の 出 現 は:=<1>と:=<2>に 分 類 さ れ ，Racket のユニットシステム [3] などのモジュール・シ

-->PCF5-red のパラメータとして抽象化されていステムを用いて，複数のコンポーネントが互いのス

る．es 間の確率的な選択は racket/random ライブラ

コープの外に分離されてしまうことがよくある．補リを用いて実装している．また，"EC"規則を子簡約

助定義の数が膨大であり，それらがいくつかの独立し関係で再利用できるよう，この簡約関係は-->でもパたコンポーネントを構成している場合，ユニットシス

ラメータ化されている（後述）．

テムは便利である．さらに，2 つのコンポーネントがPCF5 のインスタンスは次のように生成する．ここ

相互に依存しているような場合，そういった依存関係

で，:=は:=<1>と:=<2>の両方に使用される．

は Racket ユニットを使わなければ構築できない．ま(define -->PCF5* (reducer-of -->PCF5-red))

た，ユニットはコンパイル時ではなく実行時に置き(define -->PCF5 (-->PCF5* -->PCF5* := :=))

換えることもできる．例えば，様々な状況や文脈に応(define e5 '(+ (amb 1 2 3 4)

じ，単一システム内で同じ言語ファミリーの多くのバ(amb 10 20 30 40))
(apply-reduction-relation* -->PCF5 e5); ⇒ {14}(apply-reduction-relation* -->PCF5 e5); ⇒ {43}
PCF5 の子簡約関係を定義し，amb の意味をランダ
ム選択から非決定的計算へ変えてみる．まず，レキシ
カル・スコープからの逸脱を利用して select 関数のリエーションが必要とされるような場合にユニットは有益である．
ユニットシステムの一部として簡約関係を適切に操作するため，LwRed は簡約関係そのものをユニットとして実現している．簡約関係の定義が依存しているシグネチャ（Racket ユニットの importシグネチャに対応）は以下のように指定する：

(define-unit delta2@(define-reduction ....
#:within-signatures [sig ...] ....)
簡約関係ユニットは，その遷移関数を意味する名前

reducer だけからなる red^シグネチャをエクスポー(import red^) (export delta^)(define (prim? op)(member op '(+ <= eval)))(define (δ op vs)トする．
例として，まず PCF6 を複数のユニットに分割してみる．組み込み演算子に関連する補助定義の名前(define --> (reducer reducer))(case op[(eval)は delta^シグネチャに，その他の雑多な補助関数は(set-firstmisc^シグネチャに集約する：(apply-reduction-relation*(define-signature delta^ (prim? δ))(define-signature misc^--> (cadar vs)))](val? subst))

これらのシグネチャを実装するユニット定義は次のとおり：(define-unit delta1@(import) (export delta^)(define (prim? op) (member op '(+ <=))).... ; as before)))(define-unit misc2@(import delta^) (export misc^)(define (val? x)(match x(define (δ op vs) ....) ; as before[`(quote ,form) #t].... ; as before(define-unit misc1@(import delta^) (export misc^)(define (val? x) ....) ; as before(define (subst e x e*) ....)); as before))(define (subst e x e*) ....)); as before(define-values/invoke-unit/infer

これらの定義の下，簡約関係は以下のように定義でき(export red^)る．各規則の定義はこれまでと同じである：(link delta2@ misc2@ -->PCF7-red@))(define-reduction (-->PCF7-red -->)

上記の拡張では，簡約関係-->PCF7-red@を継承や上#:within-signatures (delta^ misc^)

書きによって修正する必要がまったくなく，合成する[`(,(? prim? op) ,(? val? vs) ...)

2 つの補助ユニットを置き換えるだけで済んでいる．

(δ op vs) "prim"][`((λ (,x) ,e) ,(? val? v))(subst e x v) "β"]....)Racket のユニットシステムが提供するユニットを合成・インスタンス化する通常の方法を用いることで，次のように遷移関数を生成できる：(define-values/invoke-unit/infer(export red^)(link delta1@ misc1@ -->PCF7-red@))(define -->PCF7 (reducer reducer))

3 実装
本節では，LwRed の実装について説明する．分か
りやすさのため，本節で紹介するソースコードは，実際の実装を若干簡略化したものである．

3. 1 非決定的モナド
2. 2 節で説明したとおり，define-reduction の規則本体では非決定的モナドを使用することができる．
非決定的モナドは，Racket の集合データ型 set を最後に，簡約関係と補助関数の間の相互依存の例と使って，次のように実装されている．ここで，pure

して，eval プリミティブを PCF7 に追加してみる．

と lift はそれぞれ，単一の値または値の集合をモナ

delta2@ユニットでは，インポートされている red^

ドに注入する操作である．

の reducer を介して遷移関数がインスタンス化され，(define (pure x) (set x))

再帰的に呼び出されている．

(define (lift xs) xs)

(define (bind r k)「param ...」によりパラメータ化された簡約関係 rid(apply set-union (set) (set-map r k)))は，「parm ...」をパラメータとして受け取る同名の

LwRed ユーザが規則本体を記述するのに用いる do記

関数として実現される．この関数は「状態 s を受け法は，単純な Racket マクロとして定義されている：

取り，可能な 1 ステップの簡約により生成される次状(define := (gensym)) (define <- (gensym))

態の集合を返す遷移関数」を返す．

(define (with op r k)(cond [(eq? op :=) (k r)][(eq? op <-) (bind r k)]))(define-syntax (do stx)
(syntax-case stx ()[(do s) #'s]

make-reducer-body 関数は，遷移関数本体のコードを生成する．補助関数 mk-hash は，キーと値のリストを受け取り，ハッシュテーブルを生成する．
遷移規則 [pat b ... name] のリストから mk-hash
を 使 用 し て 構 築 さ れ た 規 則 集 合 を 表 す ハッシュ[(do #:with pat op e s1 s ...)

テーブルが，make-reducer-body に渡される．次の#'(with op e

make-reducer-body では規則名（テーブルのキー）(match-lambda[pat (do s1 s ...)]))][(do #:when t s ...)

は使用されないが，3. 3 節の継承において重要な役割を果たす．

(define-for-syntax#'(if t (do s ...) (set))](make-reducer-body s cmap)[(do s1 s ...)

(for/fold ([body #'(set)])#'(begin s1 (do s ...))]))([c (in-hash-values cmap)])#:with構文の op が:=の場合は letとして機能し，<-(syntax-case c ()の場合は bind として機能する．これらの演算子は，[(pat b ... bn)

実行時に交換可能なよう，ファーストクラスなシンボ#`(let ([nexts #,body])

ルとして定義されている．

(match #,s[pat (set-unionnexts

3. 2 遷移関数
簡約操作の第一近似として，まずは継承とユニ(do b ... (pure bn)))][_ nexts]))])))

ットを考慮しない実装について考える．簡単のたマッチしたすべての節を非決定的に実行するため，

め，常にパラメータ化された簡約関係を定義する

make-reducer-body マクロは define-reduction で

define-reduction について説明する．パラメータを並列に書かれたパターンマッチを，入れ子の match式

指定しないものは，パラメータがゼロ個の特殊バーへ変換する．すべての可能な遷移は，nexts に蓄積さジョンに過ぎず，define-reduction マクロの追加のれた内側の結果と外側のマッチ結果の set-union に展開規則で簡単に扱うことができる．

より集められる．外側の 1 ステップの遷移は，非決定(define-syntax (define-reduction stx)

的モナド (do b ... (pure bn)) として実行される．

(syntax-case stx ()[(_ (rid param ...)
[pat b ... name] ...)#`(define ((rid param ...) s)#,(make-reducer-body #'s(mk-hash

最後に，遷移関数を使用して複数の遷移を実行する

apply-reduction-relation*関数は，標準的なワー
クリストアルゴリズムを使用して実装されている：(define (apply-reduction-relation* --> s)(let ([all-states (mutable-set)](syntax->datum #'(name ...))[normal-forms (mutable-set)](syntax->list[worklist (make-queue)])#'([pat b ...] ...)))))]))(define (loop)

(unless (or (queue-empty? worklist))(let* ([s (dequeue! worklist)][nexts (--> s)])(if (set-empty? nexts)(set-add! normal-forms s)(for ([next (in-set nexts)]#:when (not(set-member?
all-statesnext)))(set-add! all-states next)(enqueue! worklist next))))(loop)))(set-add! all-states s)(enqueue! worklist s)(loop)
normal-forms))
3. 3 継承
継承による拡張をサポートするには，ある簡約関係の define-reduction をマクロ展開する際，その親簡約関係（および再帰的にさらにその祖先）のdefine-reduction により指定された様々なプロパ
ティを維持する必要がある．現在の実装では，定義：(define-reduction (rid param ...)#:super (sup-id sup-arg ...)
[pat b ... name] ...)

(define-syntax (define-reduction stx)
(syntax-case stx ()[(_ (rid param ...)#:super (sup-rid arg ...)
[pat b ... name] ...)
(with-syntax([eid (fmt-id #'rid "~a@" #'rid)])#`(begin(define-syntax rid(rdesc #'eid #'(param ...)#'sup-rid #'(arg ...)
(make-hash(list (cons name#'((... ...)
[pat b ...]))...))))(define-syntax (#%reducer stx)#`(λ (param ...)(λ (s)#,(make-reducer-body#'s(syntax-local-value #'rid)#f '()))))(define eid (#%reducer))))]))
図1

継承をサポートする define-reduction

変換子（つまりマクロ）を定義するために用いられる Racket の define-syntaxは，構文変換子以外の任意の値を束縛するためにも使用できる．更新後のdefine-reduction により生成されるコードでは，定義している簡約関係の rdesc 構造体を格納するために対応し，次の rdesc 構造体を構築する．なお簡に名前 rid を使用している．生成された遷移関数を単 化 の た め ，親 簡 約 関 係 が 存 在 し な い 場 合 に は ，格納するために使用される実行時変数の名前（eid）#:super (#f) と書くものとする．

は，rid の末尾に@を付加することでつくられるフレッ
シュな識別子である †3 ．

(struct rdesc (entity params
sup-id sup-args cmap))

make-reducer-body が生成するコードは，param

entity フィールドには，対応する遷移関数（実行時

達のスコープ内部に置かなければならない．また，に使用されるファーストクラスのオブジェクト）が格

make-reducer-body は，rdesc が rid に格納され納されている実行時変数名を参照する構文オブジェク

た後にコードを生成しなければならない．仮に，eid

トが含まれる．params，sup-id，sup-args は，それを定義するコードを：ぞれ define-reduction 構文中の対応する構文オブ(define ((eid param ....) s)

ジェクトである．また，前節で mk-hash を使用して.... #,(make-reducer-body ....) ....)

構築されたのと同じハッシュテーブルがマクロ展開時の よ う に 生 成 す る と ，make-reducer-body のに構築され，cmap に格納される．
継 承 を サ ポ ー ト す る よ う 更 新 さ れ た

define-reduction の定義を図 1 に示す．主に構文†3 末尾の@は，慣例的にユニット名を表す．後述の拡張により，簡約県警の実体は単なる関数ではなくユニットとなる．

呼 出 し が 早 す ぎ る こ と に な る ．こ の 問 題 を
解 決 す る た め ，make-reducer-body の 呼 出 しを「define-reduction の マ ク ロ 展 開 時 」か ら
「define-reduction によって生成されるコードのマクロ展開時」まで遅延させる．eid とは別に定義されている#%reducer は，そのためのマクロである．

rid から遷移関数を取り出す reducer-of の定義は次の通り：

(define-syntax (reducer-of stx)
(syntax-case stx ()[(_ rid)(rdesc-entity(syntax-local-value #'rid))]))
syntax-local-value は，define-syntaxによって格納されているデータへマクロ展開中にアクセスする
ための Racket の関数であり，reducer-of の呼出しが eid への参照に置き換えられる．
継 承 を サ ポ ー ト す る よ う 更 新 さ れ た

make-reducer-body の定義を図 2 に示す．更新後の定義では，祖先簡約関係の rdesc 達を参照することにより，それらに含まれる簡約規則も再帰的に生成する．引数 maybe-args は，親簡約関係に対し再帰的に呼び出された場合にはその実引数を保持し，define-reduction から直接呼び出された場合には#f を保持している．引数 subrules には，祖先簡約関係の処理中にコードの生成を抑制するため，子孫簡約関係中に存在する簡約規則の名前の集合が含まれている．親簡約関係に対する make-reducer-body の再帰呼出しによって生成された本体コード sup-bodyに対し，子簡約関係の規則のためのコードが追加される．本体コード中のすべてのパラメータ参照 param(define-for-syntax (make-reducer-bodys rd maybe-args subrules)(match-define(rdesc _ params sup-id sup-args cmap) rd)(define sup-body(if (syntax->datum sup-id)(make-reducer-bodys (syntax-local-value sup-id)
sup-args(append subrules (hash-keys cmap)))#'(set)))(let ([args (or maybe-args #'())][params (if maybe-args params #'())])(with-syntax ([(param ...) params][(arg ...)args])#`(let-syntax([param (make-rename-transformer #'arg)]...)#,(for/fold ([body sup-body])([(nam c) (in-hash cmap)]#:unless (member nam subrules))(syntax-case c ()[(pat b ... bn)#`(let ([nexts #,body])(match #,s[pat (set-union nexts(do b ... (pure bn)))][_ nexts]))]))))))
図2

make-reducer-body の定義

datum->syntax を用いて実現する．syntax->datum
は構文オブジェクトから純粋なコード（S 式）を抽出
し，datum->syntax はある構文オブジェクトのレキ
シカル文脈データを S 式に付加することにより，新
たな構文オブジェクトを生成する．したがって，以下の rescope 関数は，stx1 のレキシカル文脈データを

stx2 に移植する：(define-for-syntax (rescope stx1 stx2)(datum->syntax stx1

が，Racket の make-rename-transformer によって(syntax->datum stx2)))生成されるリネームマクロによって，子簡約関係から

これにより，make-reducer-body によって生成され渡された名前 arg への参照に置き換えられているこるコードを任意のレキシカル文脈中に埋め込むこととに注意して欲しい．

ができる．具体的には，make-reducer-body を次のように修正する．生成されるコード中のすべての構文

3. 4 レキシカル・スコープの調整

オブジェクトは，追加の引数 ctx によって渡される

2. 3 節で説明したレキシカル・スコープからの逸レキシカル文脈データによって rescope される．

脱は，構文オブジェクト中のレキシカル文脈デー
タを操作するための Racket 関数 syntax->datum，(define-for-syntax(make-reducer-bodyctx s rd maybe-args subrules)....
(with-syntax ([(param ...)
(rescope ctx params)][(arg ...)
(rescope ctx args)])....
(syntax-case (rescope ctx c) ()[(pat b ... bn)....])))
修正後の define-reduction を以下に示す．簡約関
係名 rid を make-reducer-body の引数 ctx として渡している．この rid は，さらに make-reducer-bodyの す べ て の 再 帰 呼 び 出 し に も 渡 さ れ て お り，

define-reduction を囲む文脈中のあらゆる名前が，祖先簡約関係中で定義された簡約規則からも見えるようになる．

(define-syntax (define-reduction stx)

(define-syntax (define-reduction stx)
(syntax-case stx ()[(_ (rid param ...)#:super (sup-rid arg ...)#:within-signatures (sig ...)
[pat b ... name] ...)
(with-syntax([eid (format-id #'rid "~a@" #'rid)])#`(begin(define-syntax rid ....) ; as before(define-unit eid(import sig ...) (export red^)(define-signature M^((define-values (reducer) (#%reducer))(define-syntaxes (#%reducer)(λ (stx) ....))))(define-unit M@ (import) (export M^))(define reducer(invoke-unit(compound-unit (import) (export)(link (([m : M^]) M@)(() (unit (import M^) (export)
reducer) m)))))
reducer)))]))(syntax-case stx ()[(_ (rid param ...) ....)

図3

define-reduction の定義（最終版）(with-syntax ....
#`(begin(define-syntax (reducer-of stx)....

(syntax-case stx ()(define-syntax (#%reducer stx)#`(λ (param ...)(λ (s)#,(make-reducer-body#'rid #'s
(syntax-local-value #'rid)#f '()))))....))]))[(_ rid)#`(invoke-unit#,(rdesc-entity(syntax-local-value #'rid)))]))
define-reduction は，define-unitを用いて ユニットを定義するコードを生成する．生成されるコード中において，define-unitは#:within-signaturesで指定されたインポートされているシグネチャのレキ

3. 5 Unitization

シカル・スコープ内部に配置されなければならない．

2. 5 節で述べたように，define-reduction は実際

一方，これまで説明した実装において重要な役割を果には遷移関数を直接生成せず，次の red^シグネチャ

たしている#%reducer は，マクロとして定義されてをエクスポートするユニット定義を生成する：

いるため Racket のユニットシステムで若干問題を生(define-signature red^ (reducer))

じる．すなわち，ユニットシステムでは，マクロ定義

reducer がその遷移関数を表している．また，簡約関（define-syntax）を define-unit本体に書くことが係を実装するユニット中の最後の式は，その遷移関数

できず，代わりに，define-signatures 中に記述せを参照する式となっている．したがって，reducer-of

ざるを得なくなる．

は，invoke-unitを使って実体ユニットをインスタン
ス化するコードとして次のように定義できる：

上記の問題を解決すると同時に，前節で述べた

LwRed の設計方針を満たすため，define-reduction

を 図 3 に 示 す よ う に 修 正 し ，入 れ 子 に なった

それら 2 つシンタックスシュガーを用いて，単純な再define-unitを生成するようにする．rid の定義はこ帰算術関数からなる 3 つの小さなベンチマーク・プロ

れまでと同じである．簡約関係の実体ユニットであグラム（add，mult，ack）を用意する：

る eid の定義は，#:within-signaturesで指定され(let ([add (λ (x) (+ (car x) (cdr x)))])

たすべてのシグネチャをインポートし，red^をエク(let ([curry (λ (f) (λ (x) (λ (y)(f (cons x y)))))])

スポートする．また，生成コードには，ローカルシグ
ネチャM^とローカルユニット M@の定義も含まれている．
（M@ではなく）M^に#%reducer の定義が含まれて
おり，M@は M^と eid の間の橋渡しの役割を果たしている．M^（およびその中に含まれる#%reducer）がシ(((curry add) 5) 7)))
(letrec([mult(λ (p)(if (= (car p) 0)

グネチャ「sig ...」からインポートされている名前

0のスコープの内側に置かれていることに注意して欲し(+ (cdr p)

い．eid ユニットの遷移関係は，M@と匿名ユニットを(mult (cons (- (car p) 1)(cdr p))))))])

combine-unit によって組み合わせることで作成されたユニットを呼び出すことにより生成される．後者の
匿名ユニットが，M@からインポートした遷移関係をそのまま返している．

4 評価
本節では，LwRed と Redex [8] の実行時間を比較する．測定には 2 つの異なるプログラムセットを用(mult (cons 4 7)))
(letrec([ack(λ (m)(λ (n)(if (= m 0)(+ n 1)(if (= n 0)

いる．まず，2 節の PCF 言語で書かれたいくつかの((ack (- m 1)) 1)

小さなプログラムを，両ツールで実装された簡約関係((ack (- m 1))の上でそれぞれ実行し，その実行時間を測定する．次((ack m) (- n 1)))))))])に，より現実的な規模の遷移系として，Racket の衛生的かつ手続き的なマクロシステムの実行モデル [4]を両ツール上に実装し，その成果物 [5] に含まれているベンチマークを用いて実行時間を測定する．どちらの場合においても，Redex 上の実装は LwRed 上の実装と本質的に同じように書かれている．
測定に用いた環境は次のとおり：• ハードウェア：MacBook Pro (16-inch, M1 Max,2021)，64GB メモリ• ソフトウェア：macOS 12.6, Racket v8.6 [cs]ベンチマークの実行時間の測定には，Racket 標準ラ
イブラリの time-apply 関数を使用する．

4. 1 PCF マイクロベンチマーク
測定の準備として，let構文と letrec構文を 2 節の PCF に変換する別の遷移系を定義する．そして，((ack m) n))
図 4 に実行時間の測定結果を示す．図中，「lw」と「rx」はそれぞれ LwRed と Redex の実装を意味する．Redex で生成された遷移関数は，デフォルトでメモ化が有効になっている．まったくメモ化しない

LwRed と公平に比較するため，Redex についてはメモ化機能をオフにした実行についても測定を行った．図 4 の「rx-no-cache」がその結果である．
棒グラフは，5 つのプログラムの実行時間（ミリ秒）を示している（ack は 3 つの異なるパラメータの組で測定を行った）．図には，letと letrecの前処理を含む簡約全体の間に辿った状態の数を示す折れ線グ
ラフも含めている．apply-reduction-relation*を少し修正することで状態数を数えている †4 ．
†4 同じ PCF 実行モデルを実装しているため，rx と
rx-no-cache の状態数は lw と同じである．

LwRed のパターンマッチが rx より平均して 43 倍，

Execution time (ms) & # of states
1000000

1000

100000rx-no-cache より平均して 386 倍高速であることを示している．

10000

100

1000

パターンマッチングで大きな性能差があるが，図 4の実行時間全体と比べると，その差はそれほど顕著で

100

10

10

はなく，他の要因によっても高速化されていることがわかる．Redex の実行時間には，例えば到達可能な

1

1
add

mult

lw

図4

ack(1,6)rx

rx-no-cacheack(2,2)

ack(2,4)# of states

各状態に対するアサーションチェックのような，現在の LwRed がサポートしていない機能を実現するのに

PCF プログラムの実行結果（全体）

必要なオーバヘッドが含まれているものと思われる．

4. 2 スコープ集合モデル

Execution time of pattern-matching (ms)10000

より現実的なベンチマーク・プログラムとして，衛生的かつ手続き的なマクロをサポートするイン1000

タプリタとして表現された，Racket の形式的な実100

行モデル（スコープ集合モデルと呼ぶ）を用いることにする．スコープ集合モデルの実行可能コード

10は，ビッグステップ操作意味論に基づき Redex の
1
add

mult

ack(1,6)

lw

図5

rx

ack(2,2)

ack(2,4)

rx-no-cache

PCF プログラムの実行結果（パターンマッチのみ）

define-metafunction の集合として記述されている[5]．今回の性能比較に用いるため，それを同等のス

モールステップ簡約規則に系統的に書き換えている．
スコープ集合モデルには，前節の PCF にはないいこれらの測定結果から，lw は平均して rx より 584

くつかの特徴がある：

倍，rx-no-cache より平均して 850 倍高速であるこ

1. PCF と比較し，より広範な遷移系を形成していとがわかる．状態数と実行時間はすべての実装においる．具体的には，スコープ集合モデル全体で 56て比例している．この結果は，PCF が単純な言語実個の簡約規則があるのに対し，PCF には 13 個

行モデルであり，各状態で実行される操作の量が一定しかない．

であることを示唆している．

lw については，Racket の memoize ライブラリを

2. スコープ集合モデルにおける各状態は，PCF のような単純な項ではなく，ストア，環境，継続と使ってすべての補助関数をメモ化することも試みた

いったより複雑なデータ構造を含んでいる．

が，実行時間の改善は見られなかった．このことから，

3. 2. 5 節の最後の例のように，スコープ集合モデ

rx が rx-no-cache よりも高速である理由は，Redex

ルは評価とマクロ展開の間の相互再帰的な遷移が項のパターンマッチ処理をメモ化しているからだと関係から成る．各状態はその一部として継続を推測できる．一方，lw は Racket の matchをそのまま含み，相互再帰に伴い継続が伸び続けるため，ス

利用しているため，その実装にメモ化を追加するのはコープ集合モデルにおける全状態空間はかなり容易ではない．

の規模となる．

上記の観察に基づいてより詳細に調査するため，パ

前節と同様，スコープ集合モデルの 3 つの異なる

ターンマッチングのみを行うプログラムを用意し，そ実装（lw，rx，rx-no-cache）を用意し， [5] に含ま

れ以外はまったく同じ設定で実行速度を測定した．それる 22 個のサンプル Racket プログラムの実行時間の結果（図 5）は，メモ化を行わないにもかかわらず，を測定する．図 6 にその結果を示す．結論から述べる

Execution time (ms) & # of states
1000000

900
800

100000
700
10000

600
500

1000
400
100

300
200

10
100

lw

図6

rx

rx-no-cache

ha
do
w2
de
fs
-lo
ca
l

ha
do
w

s-s

s-s
de
f

de
f

bo
x

t-b
ox
se

xp

lb
in
de
r

to
p

t-l
e

ne
s

xp
le

le

xp
-s

lu
e

n

lva

ge

id

pr
un
e

th
un
k

hy
g

pl
e

tra
ns
re
f

#f
if-

sim

#t

t-x

if-

le

eq
?

0

<

1

# of states

スコープ集合モデルの実行結果と，lw は rx より平均して 76 倍，rx-no-cache よりなパターンマッチ機能によるものである．しかし，い平均して 580 倍高速となっている．また図からわかる

くつかの他の構成要素（例えば，評価文脈）に関連すとおり，実行時間はすべての実装（特に rx）においるアドホックな記法など，いくつかの制限によりそて状態数に対し指数的な傾向を示している．この結果の柔軟性を損なっている．また，補助定義を記述する

は，各状態遷移で実行される操作にかかる時間が定数際，通常の Racket 言語であれば当然のように記述でオーダではないことを意味する．Redex では，遷移きる高階関数は許されない．

中の複雑な操作は通常 define-metafunction によっ

Redex は 言 語 拡 張 の た め の 2 つ の 機 能て定義された別の補助関数として記述される．この構

define-extended-language と extend-reduction-

文は簡約関係と同様に Redex のパターンマッチ機能

relation を提供している．しかしながら，これらはの上に構築されているため，前節のパターンマッチ速LwRed の言語拡張の機能ほど柔軟ではなく，特に，度の測定結果からも分かるように，補助関数の実行に

親遷移規則中の名前参照を別の名前へリダイレクト実行性能のボトルネックが生じている可能性がある．

することはできない．Redex の拡張である [9] は何

一方，LwRed では，Racket ライブラリ中の効率的種類かの定義名への動的束縛を導入している．しかしなデータ型や関数を自由に使用することが可能であながら，上記の問題に対処するための能力は限定的でる．生の Racket コードを直接 Redex に埋め込むこあり，実際，スコープ集合モデルを実装するには簡約とも原理的には可能であるが，Redex と Racket の関係の定義のいくつかの部分でコードの複製が必要

記法が混在することで可読性が低下し，推奨されていであることがわかっている．

ない．

Ott [11] もまた，簡約関係を含むプログラミング言
語に関する様々な研究を支援する機能を備えた DSL

5 関連研究である．形式的に定義された遷移規則を他の言語上のRedex [8] は，簡約関係だけでなく，型システム

実行可能なコードに変換することができる．しかしな（型判断規則），遷移状態に対するアサーション，単体

がら，Redex や LwRed ほど柔軟なパターンマッチ

テストなど，意味論に関する様々な側面を表現するたを記述できず，大規模な遷移規則集合に対する拡張性めの機能を備えたプログラミング言語研究支援 DSL

も特にサポートしていない．

である．Redex の表現力は，主に S 式に対する強力

6 まとめと今後の課題
本論文では，実用的なシステムに組み込まれた遷移システムを記述するための領域特化言語である

LwRed を提案した．LwRed は，レキシカル・スコー
プから逸脱した規則本体の記述，Racket ユニットシステムとの統合などの特徴を備えており，大規模な遷移系のモジュール化され拡張可能な記述を可能としている．また，LwRed の設計はホスト言語である

Racket との互換性が高く，簡易かつ効率的な遷移規則を実現することが可能である．

Racket のパターンマッチやパターンエクスパンダを使用して簡潔な状態パターンを記述するには，Racketのマクロにある程度精通している必要がある．例えば，本論文で示したものよりさらに複雑な文脈（例えば，プロセス計算で使用されるような複数のホールを含む文脈）であっても，パターンエクスパンダとして実現することは可能である．とはいえ，このような複雑な形状の文脈をより直接的に表現するための上位 API を LwRed に追加することは，様々な遷移系を実装する労力を軽減するのに役立つものと思われ，今後の課題の一つと考えている．
謝辞 本研究は JSPS 科研費 JP20K11757 の助成を受けたものである．

参 考 文 献[ 1 ] Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, North-Holland Linguistic Series,
North-Holland, 1984.
[ 2 ] Culpepper, R. and Felleisen, M.: Fortifying
Macros, Proceedings of the 15th ACM SIGPLAN
International Conference on Functional Programming, ICFP ’10, 2010, pp. 235–246.
[ 3 ] Findler, R. B. and Flatt, M.: Modular ObjectOriented Programming with Units and Mixins, Proceedings of the Third ACM SIGPLAN International
Conference on Functional Programming, ICFP ’98,
1998, pp. 94–104.
[ 4 ] Flatt, M.: Binding as Sets of Scopes, Proceedingsof the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’16, 2016, pp. 705–717.
[ 5 ] Flatt, M.: Binding as Sets of Scopes – Notes ona new model of macro expansion for Racket, 2016.
[ 6 ] Flatt, M. and PLT: Reference: Racket, Technical Report PLT-TR-2010-1, PLT Design Inc., 2010.

https://racket-lang.org/tr1/.
[ 7 ] Horn, D. V.: An Introduction to Redex with
Abstracting Abstract Machines (v0.6), 2014.
[ 8 ] Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J. A.,
Rafkind, J., Tobin-Hochstadt, S., and Findler,
R. B.: Run Your Research: On the Eﬀectiveness ofLightweight Mechanization, Proceedings of the 39th
Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’12,
2012, pp. 285–296.
[ 9 ] Moy, C.: Redex Parameters, 2020.
[10] Plotkin, G.: LCF considered as a programming
language, Theoretical Computer Science, Vol. 5,
No. 3(1977), pp. 223–255.
[11] Sewell, P., Nardelli, F. Z., Owens, S., Peskine,G., Ridge, T., Sarkar, S., and Strniša, R.: Ott:Eﬀective Tool Support for the Working Semanticist, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming,
ICFP ’07, 2007, pp. 1–12.
[12] Wadler, P.: The Essence of Functional Programming, Proceedings of the 19th ACM SIGPLANSIGACT Symposium on Principles of Programming
Languages, POPL ’92, 1992, pp. 1–14.

A 付録: cxt パターンエクスパンダの定義
可 読 性 の た め ，以 下 の cxt の 定 義 で は ，syntax/parse ライブラリ [2] を使用している．
(begin-for-syntax(define (mask-unquote stx)
(syntax-parse stx#:datum-literals [unquote ?][(unquote (? p x)) #'(unquote (? p))][(unquote e) #'(unquote _)][(s ...) (stx-map mask-unquote #'(s ...))][s #'s]))(define (pick-id stx)
(syntax-parse stx#:datum-literals [unquote ?][(unquote (? p x)) #'(unquote x)][(s ...) (stx-map pick-id #'(s ...))][s #'s]))(define-syntax-class hole#:attributes (nam pat upat body)(pattern(~datum □)#:with nam #'□#:with pat #',_#:attr upat (λ (pat) #`,#,pat)#:with body #',nam)(pattern(e1 ... h:hole e2 ...)#:with (u1 ...)
(stx-map mask-unquote #'(e1 ...))#:with (u2 ...)
(stx-map mask-unquote #'(e2 ...))#:with (b1 ...)
(stx-map pick-id #'(e1 ...))#:with (b2 ...)
(stx-map pick-id #'(e2 ...))#:with nam #'h.nam#:with pat #'(e1 ... h.pat e2 ...)#:attr upat(λ (pat)#`(u1 ...
#,((attribute h.upat) pat)u2 ...))#:with body #'(b1 ... h.body b2 ...))))(define-match-expander cxt(syntax-parser[(_ C:id pat h:hole)#`(and #,((attribute h.upat) #'pat)(app (match-lambda[h.pat (λ (h.nam) h.body)])C))][(_ C:id pat h1:hole h2:hole ...)#'(or (cxt C pat h1)(cxt C pat h2) ...)]))