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

アトム変数を用いた名目単一化の実装
山上 隼司

菊池 健太郎

上野 雄大

大堀 淳

本稿では，アトム変数を用いた名目単一化アルゴリズムの実装に向けての取り組みを報告する．名目単一化 (nominal
uniﬁcation) は項同士がアルファ同値となるような代入を見つけ出す操作であり，通常の単一化と違い束縛変数を扱えるという特徴を持つ．Schmidt-Schaußら (2019) のアトム変数を用いた名目単一化は，置換 (permutation) の扱
いに注意しなければならないが，アトム変数を用いないこれまでの名目単一化よりも記述が簡潔になる場合が多く，表現力が高い．しかし，その実装は課題として残されていた．本研究では，Schmidt-Schaußらが提示した体系の実装に向けた再構築と，再構築した体系に基づく，関数型言語 SML#を用いた実装を行っている．本稿では，その経過を報告する．

これに対し，最近 Schmidt-Schaußら [5] が導入した

1 はじめにアトム変数を用いる名目単一化では，アトムを表す

単一化は定理証明の自動化等において用いられる

メタ変数に対応するアトム変数も代入の対象となる．

重要な技術である．近年普及している高階型理論・高

ただし，単一化問題の可解性は，条件を満たす基底代

階述語論理に基づく定理証明支援系は，束縛変数を入 (変数を含まない項を割り当てる代入) が存在する

含む言語を対象としており，そこで用いられる単一化

か否かによって判定される．アトム変数を持つ言語をでは束縛変数を伴う項を扱う必要がある．束縛機構

用いることの利点については，先行研究 [2] [5] の第 1として変数名を用いる場合には，項同士がアルファ同値 †1 となるような代入を求める手続きを与えること

章を参照されたい．

が主な目的となる．

アトム変数を用いる名目単一化の実装に向けての取り

本稿では，先行研究 [5] で課題として残されていたGabbay-Pitts による名目技法 [1] [4] に基づいて考組みの経過を報告する． [5] では推論規則に基づく単案された名目単一化 (nominal uniﬁcation) [6] [7] は，一化手続きが提案されており，それらの推論規則は，束縛変数を伴う項を対象とした単一化の一種である．

変数やアトム変数を含む項 (名目項式とよぶ) の間のそこでは，束縛される可能性のある変数はアトムとよ

等式に関する規則と，アトムの出現制約に関する規則

ばれ，アトムに関するアルファ同値性が構文の中で明の 2 つのグループに分けられる．本研究でも，それら示的に扱われるという特徴を持つ．

の推論規則に基づいて単一化手続きの実装を進める方

元々の名目単一化では，項を表す変数 (通常の意味針をとるが，実装を行うための基盤としてより適したでのメタ変数に対応する) への代入と，変数における形へ構文や規則の記述を洗練する．本稿では，特に，アトムの出現に関する制約の組が，単一化子となる．

1. 名目項式の文法の再定義と，それに沿った各種

Implementation of nominal uniﬁcation with atomvariables
Shunji Yamagami, Kentaro Kikuchi, Katsuhiro Ueno,
Atsushi Ohori, 東北大学, Tohoku University.
†1 アルファ同値性に加え，いくつかの関係を法として項を同値とする場合もある．

操作の実装に即した定義を与える．

2. アトム変数を用いる名目単一化において重要となるアトム変数置換に関する操作について，[5] で提案されている規則を拡張した新たな規則を導入し，詳しい説明を行う．

上記 1 について，先行研究と異なるのは以下の点

トム変数を用いた名目単一化手続きについて議論すである． [5](p. 48) では，名目項式の文法が次のようる．4 章では，現時点の実装と実行例について述べる．

に与えられている．

e ∶∶= A ∣ S ∣ π ⋅ A ∣ π ⋅ S ∣ ⟨f e1 ... ear(f ) ⟩ ∣ λπ ⋅ A.e

2 名目項式π ∶∶= ∅ ∣ (A B) ⋅ π

本章では，変数を含まない項 (基底名目項) と，変

しかしながら，この定義では，アトム変数置換 π に′′数やアトム変数を含む項 (名目項式) について説明す

現れるアトム変数 A を，保留アトム変数 π ⋅ A で置る．基底名目項は関数記号を含むラムダ式で表され，き換えた場合に文法エラーとなる．一方，単一化手

アルファ同値性は基底名目項の間の関係として定義さ続きを実装する際に，単独のアトム変数 A(あるいはれる．名目項式について説明した後，アトム変数置換

変数 S) と ∅ ⋅ A(あるいは ∅ ⋅ S) を同一視すべき場面に関する注意点を述べる．

でも，構文的に区別されており，実装が煩雑になる．
そのため，上記の文法は，実装のための基盤としては

2. 1 基底名目項

適していないと考えられる． [5] では，アトム変数置

関数記号の集合を F とする．関数記号は f ，g 等換に現れるアトム変数に対する場合に限り，(保留アで表され，0 以上のアリティを持つ．関数記号 f のア

トム変数ではなく) 単独のアトム変数を代入するようリティを ar(f ) と書く．また，アトムの集合を At とに注意深く制限することにより，単一化手続きを構成する．アトムは a，b などで表され，名前の異なるア

することが可能であるとしている．しかし，本研究でトム同士は互いに異なるアトムとする．F と At は互

は，アトム変数置換における保留アトム変数の出現をいに共通の要素を持たない．基底名目項はアトム，関許す，より広い文法を採用することにする．

数記号，アトムを束縛するラムダ式で構成される．

他の先行研究 [2] [3] では，本稿と同様にアトム変数
置換における保留アトム変数の出現を許す形で名目項式の文法を与えている (v ∶∶= π ⋅ A のような保留ア

定義 1. 基底名目項の集合 NLa は以下の文法で定義される．

e ∈ NLa ∶∶= a ∣ ⟨f e1 ... ear(f ) ⟩ ∣ λa.e

トム変数の構文カテゴリを加えている)．しかし，本⟨f e1 ... ear(f ) ⟩ は関数適用を表す．以下ではタ

稿の定義 6 で見るような代入の再帰的な定義は与え

プ ル ⟨e1 ... ear(f ) ⟩ も 用 い る が ，こ れ は 関 数 適 用

られておらず，単一化手続きの実装についても触れら⟨f e1 ... ear(f ) ⟩ の関数名が無い場合とみなす．

れていない．

二つのアトム a と b を入れ替える操作を互換 (swap-

アトム変数置換に関する操作について先行研究とping) と言い，(a b) で表す．定義域 dom(τ ) = {a ∈異なるのは以下の点である． [5](p. 53) で注意されてAt ∣ τ (a) ≠ a} が有限集合となるような At 上のいるように，アトム変数置換を構成する列の要素は，

全単射 τ を，置換 (permutation) と言う．置換は，条件を満たす場合に順番を入れ替えることが可能で互換の有限列で表すことができる．置換 τ をアト

ある．しかし，それをそのまま規則として取り入れた

ム a に適用することを τ ⋅ a と表し，このとき列の場合，全体の手続きの停止性を妨げてしまう． [5] で

右から順に互換をアトムに適用していく．例えばは，入れ替えを行う規則は導入しないが，それに修正

置換 τ = (a b)(a c) をアトム c に適用する場合は，を加えた場合，実装におけるアトム変数置換の簡単化τ ⋅ c = (a b)(a c) ⋅ c = (a b) ⋅ a = b となる．

に効果的であり得るとしている．本研究では，そのよ

定義 2. 置換を NLa の項へ適用する関数 ⊙ を，以下

うな入れ替えを他の規則と適切に組み合わせることのように定義する．

により， [5] で示唆されていることを実現するいくつかの新しい規則を導入した．

τ ⊙ a ∶= τ ⋅ aτ ⊙ ⟨f e1 ... ear(f ) ⟩ ∶= ⟨f τ ⊙e1 ... τ ⊙ear(f ) ⟩本論文の構成は以下の通りである．2 章では，基底τ ⊙ (λa.e) ∶= λ(τ ⋅ a).(τ ⊙ e)

名目項と名目項式の基本事項を述べる．3 章では，ア

アトム a と基底名目項 e の組 a#e を非出現関係

する．

e ∈ NLAS ∶∶= π ⋅ A ∣ π ⋅ S ∣ ⟨f e1 ... ear(f ) ⟩ ∣ λπ ⋅ A.e⊢NLa a#b⋯⊢NLa a#e1

π ∶∶= ∅ ∣ (π ′ ⋅ A π ′′ ⋅ B) ⋅ π⊢NLa a#ear(f )π ⋅ A を 保 留 ア ト ム 変 数 (suspensions of atom-⊢NLa a#⟨f e1 ... ear(f ) ⟩⊢NLa a#λa.e
図1variables) とよび，(π ′ ⋅ A π ′′ ⋅ B) をアトム変数互換(atom-variable swapping) と言う．アトム変数互換⊢NLa a#e⊢NLa a#λb.eの有限列 π をアトム変数置換 (atom-variable permu-

tation) と言う．また，π ⋅ S を保留変数 (suspensions

NLa 上の非出現関係の定義

of expression-variables) とよぶ．二つのアトム変数
置換 π と π ′ の連結を π ○ π ′ ，アトム変数置換 π の逆順の列を π −1 と書く．

⊢NLa a ∼ a⊢NLa e1 ∼ e′1⋯⊢NLa ear(f ) ∼ e′ar(f )⊢NLa ⟨f e1 ... ear(f ) ⟩ ∼ ⟨f e′1 ... e′ar(f ) ⟩⊢NLa (a b) ⊙ e ∼ e′

⊢NLa e ∼ e′
⊢NLa λa.e ∼ λa.e
図2′⊢NLa b#e⊢NLa λa.e ∼ λb.e′

NLa 上のアルファ同値性の定義

こ こ で ，二 種 類 の 代 入 を 定 義 す る ．ま ず，写 像ρ ∶ (A ∪ S) → NLa を基底代入 (ground substitution)と言う．基底代入はアトム変数にアトムを，変数にNLa の項を割り当てる写像である．
定義 4. 名目項式 e ∈ NLAS と基底代入 ρ について，e に ρ を適用して得られる NLa の項を eρ と書き，以下のように定義する．

(freshness relation) とよぶ．これは，アトム a が基

(π ⋅ A)ρ ∶= πρ ⋅ ρ(A)底名目項 e に自由アトムとして現れないことを意味(π ⋅ S)ρ ∶= πρ ⊙ ρ(S)する．アトムと NLa の項の関係 # を図 1 のように定⟨f e1 ... ear(f ) ⟩ρ ∶= ⟨f e1 ρ ... ear(f ) ρ⟩

義する．

(λπ ⋅ A.e)ρ ∶= λ(πρ ⋅ ρ(A)).(eρ)

また，NLa 上の関係 ∼ を図 2 のように定義する．
これは，通常の意味でのアルファ同値性 (束縛アトム∅ρ ∶= ∅((π ′ ⋅ A π ′′ ⋅ B) ⋅ π)ρ ∶=の名前替えにより到達できる関係) と一致する [1]．

(π ′ ρ ⋅ ρ(A) π ′′ ρ ⋅ ρ(B)) ⋅ πρ例えば，e = (∅ ⋅ A ∅ ⋅ B) ⋅ C ，ρ = {A ↦ a, B ↦2. 2 名目項式b, C ↦ a} のとき，eρ = (∅ρ ⋅ ρ(A) ∅ρ ⋅ ρ(B)) ⋅ ρ(C) =名目項式の集合 NLAS を定義するために，変数と(a b) ⋅ a = b ∈ NLa となる．空列 ∅ は恒等置換を表す

アトム変数を導入する．名目項式は，基底名目項を変数とアトム変数，アトム変数置換を用いて改変したものである．

ことに注意する．
また，写像 σ ∶ (A∪S) → NLAS を単に代入 (substi-

tution) と言う．この代入はアトム変数に保留アトム

変数の集合を S とする．変数は S や T で表され変数を，変数に NLAS の項を割り当てる写像である．

る．また，アトム変数の集合を A とする．アトム変定義 5. アトム変数置換を NLAS の項へ適用する関数は A や B で表される．アトム変数は NLa におけ

数 ● を，以下のように定義する．

るアトムに対応する変数であり，以下で説明するアト

π ● (π ′ ⋅ A) ∶= (π ○ π ′ ) ⋅ A

ム変数からアトムへの代入 (基底代入) によって，アπ ● (π ′ ⋅ S) ∶= (π ○ π ′ ) ⋅ S

トムでのみインスタンス化される変数である．S とA，また F は互いに共通の要素を持たない．
定義 3. 名目項式の集合 NLAS を以下の文法で定義

π ● ⟨f e1 ... ear(f ) ⟩ ∶= ⟨f π●e1 ... π●ear(f ) ⟩π ● (λπ ′ ⋅ A.e) ∶= λ(π ○ π ′ ) ⋅ A.(π ● e)
定義 6. 名目項式 e ∈ NLAS と代入 σ について，e にσ を適用して得られる項 eσ ∈ NLAS を以下のように

代入 ρ について，ρ(A) と ρ(B) の関係にかかわらず，

定義する．

((∅ ⋅ A ∅ ⋅ B) ⋅ A)ρ = (ρ(A) ρ(B)) ⋅ ρ(A) = ρ(B) とな(π ⋅ A)σ ∶= πσ ● σ(A)る．よってこれは，基底代入前に (∅⋅A ∅⋅B)⋅A = ∅⋅B(π ⋅ S)σ ∶= πσ ● σ(S)と計算しておいても結果は変わらない．アトム変数⟨f e1 ... ear(f ) ⟩σ ∶= ⟨f e1 σ ... ear(f ) σ⟩を用いた名目単一化の手続きでは，このような NLAS

(λπ ⋅ A.e)σ ∶= λ(πσ ● σ(A)).(eσ)

アトム変数置換のアトム変数への適用が保留になっ∅σ ∶= ∅′

上でのアトム変数置換の計算を多く用いる．

ている状態を表すのが，保留アトム変数である．な′′((π ⋅ A π ⋅ B) ⋅ π)σ ∶=(π ′ σ ● σ(A) π ′′ σ ● σ(B)) ⋅ πσ

お，単なるアトム変数は ∅ ⋅ A で表すことができるた

例えば，e = π ⋅ S ，σ = {S ↦ λ(π ′ ⋅ A).(∅ ⋅ T )}め，アトム変数を保留アトム変数と別で文法に取り入のとき，eσ = πσ ● σ(S) = πσ ● λ(π ′ ⋅ A).(∅ ⋅ T ) =λ((πσ ○ π ′ ) ⋅ A).(πσ ⋅ T ) ∈ NLAS となる．
′′

以下では二つの代入 σ ，σ の合成を σ ○ σ と書く．
′′

このとき，e(σ ○ σ ) = (eσ)σ であることに注意する．

れる必要はない．
また，アトム変数置換 π の変数 S への適用 π ⋅ S は
これ以上計算することはできない．このようなアトム
変数置換の変数への適用が保留になっている状態を表同様に代入 σ と基底代入 γ の合成も σ ○ γ と書き，こすのが，保留変数である．なお，単なる変数も ∅ ⋅ Sのとき，e(σ ○ γ) = (eσ)γ である．

で表すことができるため，変数を保留変数と別で文法

また，アトム変数 A と名目項式 e の組 A#e を非出
現制約といい，非出現制約の集合 ∇ を非出現制約集
合という．非出現制約集合 ∇ が A#∅ ⋅ B と A#∅ ⋅ Sの形の非出現制約のみからなるとき，その ∇ は標準
化 (standardized) されているという．

に取り入れる必要はない．

3 アトム変数を用いた名目単一化
本章では，アトム変数を用いた名目単一化の手続きについて議論する．以下では， [5] で提案されている推論規則に基づく非決定的な手続きを，前章の構文に

2. 3 アトム変数置換対応させたものを考える．推論規則は， [5] と同様に，

アトム変数置換は，基底代入後のアトムについての

NLAS 上の等式に関する規則群 AVNOM UNIFY と非出置換を表すものであり，アトム変数同士の置換を表す

現制約集合に関する規則群 AVSOL NABLA から成る．

ものではないことに注意する．例えばアトム変数置換

AVSOL NABLA は，AVNOM UNIFY で等式の集合が空

π = (∅ ⋅ A ∅ ⋅ B) は，π に任意の基底代入 ρ を適用しになった場合に呼び出される副手続きである．ここた後，(∅ ⋅ A)ρ と (∅ ⋅ B)ρ の置換を行うことを表す．

では，本研究で一部実装を終えている AVSOL NABLA

よってアトム変数同士の基底代入後の関係が明らかにのみ扱う．AVNOM UNIFY については [5](§4.3) を参照

なっていないうちは，置換をアトムに適用するかのよ

されたい．

うに，アトム変数置換をアトム変数に適用することはできない．例えば，(∅ ⋅ A ∅ ⋅ B) ⋅ C は，基底代入 ρについて，ρ(A) = ρ(C) の場合と ρ(B) = ρ(C) の場

3. 1 名目単一化問題
まず，名目単一化問題とその解，単一化子を定義

合，またこれらのどちらでもない場合とで適用結果が

する．

変わる．

定義 7. NLAS 上の等式 e1 ≐ e2 (e1 , e2 ∈ NLAS ) の集

しかし逆に，アトム変数同士の基底代入後の関係が合を Γ，非出現制約集合を ∇ としたとき，アトム変数

明らかになっていれば，置換をアトムに適用するのとを用いた名目単一化問題 (a variable-atom nominal

同じように，アトム変数置換をアトム変数に適用でき

uniﬁcation problem，以下 VANUP) を (Γ, ∇) と定る場合もある．例えば，(∅⋅A ∅⋅B)⋅A は，任意の基底

義する．
定義 8. ある基底代入 ρ が VANUP(Γ, ∇) の解 (so-lution) であるとは，すべての等式 e1 ≐ e2 ∈ Γ に対しかを判定するアルゴリズムである．AVSOL NABLA はて ⊢NLa e1 ρ ∼ e2 ρ であり，かつ，すべての非出現制

後述する九つのルールから成っており，ここではまず

約 A#e ∈ ∇ に対して ⊢NLa ρ(A)#eρ となるときをい重要な三つのルール (Rew1)，(Rew2)，(Simp) につう．VANUP(Γ, ∇) が解を持つとき，その (Γ, ∇) はいて説明する．

可解 (solvable) であるという．また (∅, ∇) が可解でアトム変数置換 π と保留アトム変数 π ⋅ A を簡単化あるとき，その ∇ は可解であるという．

するルール (Rew1)，(Rew2) を図 3 に示す．これら

定義 9. VANUP(Γ, ∇) について，ある代入 σ と非のルールは，アトム変数置換をより短い形に変形した出現制約集合 ∇′ の組 (σ, ∇′ ) が以下を満たすとき，り，アトム変数置換をアトム変数に適用することで，′その組 (σ, ∇ ) を VANUP(Γ, ∇) に対する単一化子

アトム変数置換や保留アトム変数を簡単化する．
ルール 1 は，同じ保留アトム変数同士のアトム変(uniﬁer) であるという．
′∇ が可解であり，かつ，任意の基底代入 γ につい′

数互換を削除するルールである．同じ保留アトム変数て，(∀A#e ∈ ∇ . ⊢NLa (σ(A))γ#eσγ) ならば，σ ○ γ同士のアトム変数互換は恒等置換となるため，空列 ∅が (Γ, ∇) に対する解となる．

と同義である．
ルール 2 は，アトム変数置換を最小限の数のアト

3. 2 名目単一化手続き

ム変数互換で表現するルールである．アトムについて

本節では，前章の構文に適合させ，新たな規則を取の置換 τ は，((τ に含まれるアトムの数 ) − 1) 個以下り入れた AVSOL NABLA について詳しく述べる．まの互換の列で表すことができる．一定の条件を満たせず，以下で用いる表記や記号を説明する．

ば，アトム変数置換においてもこの性質を当てはめ

非出現制約集合 ∇ について，A#(π −1 ○π ′ )⋅B ∈ ∇ ま
たは B#(π′−1′○π)⋅A ∈ ∇ であるとき，∇ ⊢ π⋅A ≠ π ⋅B′と書く．特に，∇ ⊢ ∅ ⋅ A ≠ π ⋅ B の場合は空列 ∅ を′省略し，∇ ⊢ A ≠ π ⋅ B と書く．

ることができる．ルール 2 ではこの性質を利用して，アトム変数置換に含まれるアトム変数互換の数を最小限にする．詳しくは実装の章で説明する．
ルール 3 は，アトム変数置換を保留アトム変数に適保留アトム変数の集合 M1 ，M2 について，M1 と用するルールである．ある保留アトム変数について，

M2 に含まれるすべての保留アトム変数の組 π⋅A ∈ M1 ，アトム変数置換の中に (π ⋅ A π ′ ⋅ B) が含まれており，

π ′ ⋅ B ∈ M2 に対して ∇ ⊢ π ⋅ A ≠ π ′ ⋅ B であるとき，かつその右側のアトム変数置換が π ，アトム変数が A∇ ⊢ M1 #M2 と書く．

となっているとき，(π ⋅ A π ′ ⋅ B) を右側の π ⋅ A の部

保留アトム変数の集合 M について，M に含まれ′るすべての保留アトム変数の組 π ⋅ A，π ⋅ B ∈ M に対′分に適用することができる．このときの適用結果は

π ′ ⋅ B である．

して ∇ ⊢ π ⋅ A ≠ π ⋅ B であるとき，∇ ⊢ #M と書く．

ルール 4 は，保留アトム変数 π ⋅ A について，π に

定義 10. アトム変数置換 π について，保留アトム変含まれる A と関係のないアトム変数置換を削除す数の集合 SusAt(π) を以下のように定義する．

るルールである．例えば (∅ ⋅ C ∅ ⋅ D) ⋅ A について，∇ ⊢ {A}#{∅⋅C, ∅⋅D} のとき，どんな基底代入 ρ に対

SusAt(∅) ∶= ∅
′

′′

′

′′

SusAt((π ⋅ A π ⋅ B) ⋅ π) ∶= {π ⋅ A, π ⋅ B}
∪ SusAt(π)

しても，ρ(A) ≠ ρ(C) かつ ρ(A) ≠ ρ(D) である．よって (∅ ⋅ C ∅ ⋅ D) ⋅ A は，どんな基底代入 ρ に対しても結

例えば，π = (∅ ⋅ A ∅ ⋅ B)((∅ ⋅ C ∅ ⋅ D) ⋅ A ∅ ⋅ B)

果は ρ(A) となる．このような場合，アトム変数置換のとき，SusAt(π) = {∅ ⋅ A, ∅ ⋅ B, (∅ ⋅ C ∅ ⋅ D) ⋅ A}(∅ ⋅ C ∅ ⋅ D) は基底代入前に削除しても結果は変わらとなる．

ない．このようなアトム変数置換を削除するルールが，AVSOL NABLA は，非出現制約集合 ∇ と代入 θ のルール 4 である．またこのルールは ((∅⋅C ∅⋅D)○π)⋅A組 (∇, θ) を入力とし，非出現制約集合 ∇ に代入 θ をのように，削除対象となるアトム変数置換とアトム

適用した結果得られる非出現制約集合が可解かどう

変数との間に別のアトム変数置換 π が挟まっていて(Rew1)，(Rew2)∇

1. (π ⋅ A π ⋅ A) → ∅∇2. π → π ′

π に含まれるすべての保留アトム変数のアトム変数置換が ∅ であり，かつ ∇ ⊢ #SusAt(π)

であり，かつ π に含まれるアトム変数互換の数が ∣SusAt(π)∣ 以上であり，かつ π ′ が π と同じアトム変数置換を表すもので，π ′ に含まれるアトム変数互換の数が ∣SusAt(π)∣ 未満のとき∇

3. (π ′′ ○ (π ⋅ A π ′ ⋅ B) ○ π) ⋅ A → (π ′′ ○ π ′ ) ⋅ B∇

4. (π ○ (π ′ ⋅ C π ′′ ⋅ D) ○ π ′′′ ) ⋅ A → (π ○ π ′′′ ) ⋅ A(∇ ⊢ {A}#{π ′ ⋅ C, π ′′ ⋅ D}) ∧ (∇ ⊢ {π ′ ⋅ C, π ′′ ⋅ D}#SusAt(π ′′′ )) のとき．
∇

5. π ′′ ○ (π ⋅ A π ′ ⋅ B) ○ π ′′′ ○ (π ⋅ A π ′ ⋅ B) ○ π ′′′′ → π ′′ ○ π ′′′ ○ π ′′′′
図3∇ ⊢ {π ⋅ A, π ′ ⋅ B}#SusAt(π ′′′ ) のとき(Rew1)，(Rew2) の定義

も，条件を満たせば削除することができる．例えば

ルール 1 は，関数適用に対する非出現制約を，関((∅⋅ C ∅⋅ D)○π)⋅A について ∇ ⊢ {A}#{∅⋅ C, ∅⋅ D}

数適用の中に含まれる各名目項式に対する非出現制であり，かつ ∇ ⊢ {∅⋅C, ∅⋅D}#SusAt(π) が成り立っ約に分解するルールである．このとき，関数記号のみているとき，(∅ ⋅ C ∅ ⋅ D) と π は互いに異なる保留アについての非出現制約は生成しないことに注意する．

トム変数に対する操作であるため，順番を入れ替えて

ルール 2 は，ラムダ式の中に関数適用が含まれても適用結果に影響はない．つまり ((∅⋅C ∅⋅D)○π)⋅Aいる非出現制約を，ラムダ式ごと関数適用の中の各名と (π ○ (∅ ⋅ C ∅ ⋅ D)) ⋅ A は同義である．よってこの場

目項式に対する非出現制約に分解するルールである．

合も，A と関係のないアトム変数置換 (∅ ⋅ C ∅ ⋅ D)

これもルール 1 同様，関数記号のみについての非出を削除することができる．このようにルール 4 では

現制約は生成しないことに注意する．

条件を満たしていればアトム変数置換の順番を入れ

ルール 3 は，非出現制約の左辺のアトム変数が，右替えることができるため，削除対象のアトム変数置

辺でラムダ式によって束縛されているとき，その非出換とアトム変数との間に別のアトム変数置換が挟まっ現制約を削除するルールである．非出現制約 A#e は，ている場合でも，対象のアトム変数置換を削除する．

基底代入 ρ が非出現関係 ⊢NLa ρ(A)#eρ を満たすとルール 5 は，同一のアトム変数置換を打ち消しあっていう制約を示すものである．しかし A#λ∅ ⋅ A.e は，′′削除するルールである．例えば (π⋅A π ⋅B)(π⋅A π ⋅B)

任意の基底代入 ρ に対して ⊢NLa ρ(A)#λρ(A).eρ とは同一のアトム変数置換が連続しているため，全体なり，どんな基底代入を適用しても非出現関係が成立として恒等置換になっている．ルール 5 はこのようする，意味の無い制約である．ルール 3 はこのようなアトム変数置換を削除する．またルール 4 と同様な非出現制約を削除する．

の理由から，ルール 5 でも条件を満たしていればアルール 4 は，右辺にアトム変数と変数を含まない

トム変数置換の順番を入れ替えることができるため，非出現制約を削除するルールである．右辺にアトム変間に別のアトム変数置換が挟まっている場合でも，条数と数を含んでいない非出現制約は，ルール 3 で削件を満たしていれば同一のアトム変数置換同士を打除する非出現制約同様，任意の基底代入に対して非出

ち消しあって削除する．

現関係が成立する，意味の無い制約である．ここで，次に，非出現制約 A#e を簡単化するルール (Simp)

ラムダ式のラムダの直後のアトム変数は，このルール

を図 4 に示す．このルールは，非出現制約に含まれるの条件に関わるアトム変数として数えないことに注

名目項式 e を簡単化したり，非出現制約の右辺に含ま意する．ラムダ式のラムダの直後のアトム変数が存在れるアトム変数置換を左辺のアトム変数に適用する

しても，それ以降に続く名目項式の中にアトム変数やことで，非出現制約を簡単化する．

変数が存在しなければ，その制約は意味の無い制約で

(Simp)#

1. {A#⟨f e1 ... ear(f ) ⟩} ⊍ ∇ → {A#e1 , ... , A#ear(f ) } ⊍ ∇#2. {A#λπ ⋅ B.⟨f e1 ... ear(f ) ⟩} ⊍ ∇ → {A#λπ ⋅ B.e1 , ... , A#λπ ⋅ B.ear(f ) } ⊍ ∇#3. {A#λ∅ ⋅ A.e} ⊍ ∇ → ∇#4. {A#e} ⊍ ∇ → ∇e が (ラムダ抽象以外の) アトム変数と変数をどちらも含まないとき#

5. {A#λπ ⋅ B.e} ⊍ ∇ → {A#e} ⊍ ∇∇⊢A≠π⋅B#

6-a. {A#((∅ ⋅ A π ⋅ B) ⋅ π ′ ) ⋅ X} ⊍ ∇ → {B#(π −1 ⋅ π ′ ) ⋅ X} ⊍ ∇#′6-b. {A#λ((∅ ⋅ A π ⋅ B) ⋅ π ) ⋅ C.e} ⊍ ∇ → {B#λ(π
′′

′

#

′′′

−1

′

⋅ π ) ⋅ C.((π′′(X はアトム変数または変数)−1⋅ (∅ ⋅ A π ⋅ B)) ⋅ e)} ⊍ ∇′′′7-a. {A#(π ○ (π ⋅ D π ⋅ E) ○ π ) ⋅ X} ⊍ ∇ → {A#(π ○ π ) ⋅ X} ⊍ ∇′′(X はアトム変数または変数)′′(∇ ⊢ {A}#{π ⋅ D, π ⋅ E}) ∧ (∇ ⊢ {π ⋅ D, π ⋅ E}#SusAt(π )) のとき#

7-b. {A#λ(π ′′ ○ (π ⋅ D π ′ ⋅ E) ○ π ′′′ ) ⋅ F.e} ⊍ ∇ → {A#λ(π ′′ ○ π ′′′ ) ⋅ F.((π ⋅ D π ′ ⋅ E) ⋅ e)} ⊍ ∇(∇ ⊢ {A}#{π ⋅ D, π ′ ⋅ E}) ∧ (∇ ⊢ {π ⋅ D, π ′ ⋅ E}#SusAt(π ′′ )) のとき
図4(Simp) の定義

ある．

適用することに注意する．

ルール 5 は，ラムダ式で束縛されているアトム変ルール 7-a，7-b は，右辺に含まれる，左辺のアト数が，左辺のアトム変数と非出現制約で結ばれている

ム変数に関係のないアトム変数置換を削除するルー

場合，そのラムダ式に対する非出現制約を，ラムダ式

ルである．これらは (Rew1)，(Rew2) のルール 4 との中の名目項式に対する非出現制約に変更するルール

よく似ている．(Rew1)，(Rew2) のルール４は保留アである．例えば A#λπ ⋅ B.e について，∇ ⊢ A#π ⋅ B

トム変数 π ⋅ A について A と関係のないアトム変数置のとき，任意の基底代入 ρ について ρ(A) ≠ (π ⋅ B)ρ

換を削除したが，(Simp) のルール 7-a，7-b は非出現である．よって ⊢NLa ρ(A)#λ(π ⋅ B)ρ.eρ は図 1 の定

制約 A#e について，e に含まれる A と関係のないア

義より，⊢NLa ρ(A)#eρ に置き換えられる．つまり

トム変数置換を削除する．7-a は右辺が保留アトム変この場合，A#λπ ⋅ B.e は A#e と同義である．ルー

数または保留変数の場合であり，7-b は右辺がラムダ

ル 5 はこのように，ラムダ式に対する非出現制約を式の場合である．7-b も 6-b と同様に，右辺のラムダ

変形する．

式のアトム変数の束縛の関係を保つために，適用後のルール 6-a，6-b は，右辺のアトム変数置換を左辺ラムダ式に含まれる名目項式にも，削除するアトムのアトム変数に適用するルールである．例えば 6-a

変数置換を適用することに注意する．また (Rew1)，

は，右辺が保留アトム変数または保留変数の場合であ(Rew2) のルール 4 やルール 5 同様，条件を満たせばり，アトム変数置換の一番左のアトム変数互換に，空アトム変数置換の順番を入れ替えることができるた

列と左辺のアトム変数の組の保留変数が含まれている

め，削除対象のアトム変数置換の左側に別のアトム変ならば，そのアトム変数互換を右辺から削除し，左辺数置換が挟まっている場合でも，条件を満たしていれに適用する．このとき左辺の適用結果の保留アトム変ば対象のアトム変数置換を削除する．

数のアトム変数置換は，逆順にして右辺に移項する．

AVSOL NABLA は以上の (Rew1)，(Rew2)，(Simp)

ルール 6-b はルール 6-a の右辺がラムダ式の場合での三つのルールを含む，計九つのルールからなる．

あり，ラムダの直後の保留アトム変数のアトム変数置

AVSOL NABLA を図 5 に示す．図中では [π ⋅ B/A] と換について 6-a と同様の操作を行う．このとき，右辺いう表記を用いているが，これはアトム変数 A への保のラムダ式のアトム変数の束縛の関係を保つために，

留アトム変数 π ⋅ B の代入操作を表す．また，[π ′ /π]

ラムダ式に含まれる名目項式にもアトム変数互換を

はアトム変数置換 π をアトム変数置換 π ′ で置き換え

AVSOL NABLA(Rew1)(Rew2)(∇, θ)(∇, θ)[π ′ /π](∇, θ)(∇, θ)[π ′ ⋅ A′ /π ⋅ A]
(Simp)(∇, θ)(∇′ , θ)(FreshnessFail)∇π → π ′ のとき∇

π ⋅ A → π ′ ⋅ A′ のとき#∇ → ∇′ のとき(Γ, ∇ ⊍ {A#∅ ⋅ A}, θ)Fail

他のどのルールも適用できず，(∇, θ)
かつ A1 ，A2 が ∇ か(GuessEQFC)(∇[∅ ⋅ A2 /A1 ], θ[∅ ⋅ A2 /A1 ]) ∣ (∇ ⊍ {A1 #∅ ⋅ A2 }, θ)θ の定義域以外に現れているとき(NSubst1)(∇ ⊍ {A#π ⋅ S}, θ ∪ {S ↦ e})
S が θ の中に現れていないとき(∇ ⊍ {A#π ● e}, θ ∪ {S ↦ e})(NSubst2)(NSubst3)(∇, θ ⊍ {A ↦ ∅ ⋅ B})(∇[∅ ⋅ B/A], θ[∅ ⋅ B/A])(∇, θ ⊍ {V ↦ e})
V (A または S) が ∇ と θ のどちらにも現れないとき(∇, θ)(Sat)∇ が標準化されていて，かつ θ が空であり，(∇, θ)”satisﬁable” かつ (FreshnessFail) が適用できないとき
図5

AVSOL NABLA の定義

る操作，[π ′ ⋅ B/π ⋅ A] は保留アトム変数 π ⋅ A を保留′

アトム変数 π ⋅ B で置き換える操作を表す．

任意の基底代入 ρ について ρ(A) = ρ(B) と仮定した場合の (∇[∅ ⋅ B/A], θ[∅ ⋅ B/A]) と，ρ(A) ≠ ρ(B)(FreshnessFail) は，非出現制約集合 ∇ が可解でなと仮定した場合の (∇ ⊍ {A#∅ ⋅ B}, θ) の両方を出い場合に Fail を返し，アルゴリズムを終了するルー

力する．これにより，それぞれの分岐について再びルである．具体的には，∇ が A#∅ ⋅ A の形の非出現

AVSOL NABLA の適用を進めていくことができるよう制約を含んでるときに，この非出現制約集合は可解でになり，AVSOL NABLA は最終的にそれぞれの分岐にはないと判断し，アルゴリズムを終了する．

ついての結果を出力する．AVSOL NABLA の他のどの(GuessEQFC) は，AVSOL NABLA の他のどのルー
ルも適用できないときに，(∇, θ) に含まれる二つのアルールも適用できないときにのみ，(GuessEQFC) が適用できることに注意する．

トム変数同士の基底代入後の関係を仮定することで，(NSubst1) と (NSubst2) は，θ を ∇ に適用するルー

アルゴリズムの適用を進めるためのルールである．例

ルである．(Nsubst1) は変数への名目項式の項の代えば入力 (∇, θ) について，∇ = {A#λ∅ ⋅ B.e}，θ = ∅入，(NSubst2) はアトム変数への保留アトム変数ののとき，この (∇, θ) にはこれ以上 (GuessEQFE) 以

代入を行う．(NSubst2) は，代入後の保留アトム変数

外の AVSOL NABLA のルールを適用することはできなのアトム変数置換が空列 ∅ の場合にのみ適用するこい．このようなときに (GuessEQFC) を適用すると，とに注意する．(NSubst3) は，適用先のない代入を削除するルールである．

a → b → a → ... と c → d → c → ... という二つの循環(Sat) は，(∇, θ) が可解だった場合に “satisﬁable”に分かれる．いずれにせよ，置換 τ の関数としての振を返し，アルゴリズムを終了するルールである．∇ がる舞いは必ずこのような一つ以上の循環で表すことが標準化されていて θ が空のとき，(FreshnessFail) ができ，この循環は (( 循環に含まれるアトムの数 )−1)

適用できなければ，その (∇, θ) は可解であると判断

個の互換の列で表すことができる．例えば a → b →し，アルゴリズムを終了する．

c → a → ... は (a c)(a b) で，a → b → a → ...

AVSOL NABLA は以上のルールを，Fail か “satisﬁ-

は (a b) で ，c → d → c →... は (c d) で 表 せable” か出力されるまで繰り返し適用する．次章では，る．これを利用すると，アトムについての置換 τ

この AVSOL NABLA のルールの一部を実装した結果は必ず，((τ に含まれるアトムの数 ) − 1) 個以下の互について報告する．

換の列で表すことができる．例えば，これまでの議論より，(a b)(a c)(b c)(a b) は (a c)(a b) で，

4 実装と実行例
4. 1 実装(a b)(b c)(c d)(b d) は (a b)(c d) で表せる．
アトム変数置換 π に含まれるすべての保留アト

本研究では関数型言語 SML#を用いて実装を行っム 変 数 の ア ト ム 変 数 置 換 が ∅ で あ り，か つ ∇ ⊢ている．実装の計画としてはまず AVSOL NABLA の#SusAt(π) であれば，この性質をアトム変数置換 π

実装を行い，その後 AVNOM UNIFY の実装を行う．

にも当てはめることができる．(Rew1)，(Rew2) のAVSOL NABLA の方針は以下の通りである．1．入力

ルール 2 では上の条件に加えて，アトム変数置換 πに対して (Rew1)，(Rew2)，(Simp)，(FreshnessFail)に含まれるアトム変数互換の数が ∣SusAt(π)∣ 以上

を，出力が変化しなくなるか，FreshnessFail の例外である場合に，この性質を利用してアトム変数互換が返ってくるまで繰り返し適用する．2．(Sat) を適の数を最小限にする．実装においては，アトム変数

用できるか確かめる．適用できたら終わり．適用

置換 π に含まれるすべての保留アトム変数に π をできなければ 3 に続く．3．(NSubst1)，(NSubst2)，

適用してすべての循環を見つけ，それぞれの循環を(NSubst3) のいずれかを適用する．どれも適用でき(( 循環に含まれるアトム変数の数 ) − 1) 個のアトム

ない場合は (GuessEQFC) を適用する．4．1 に戻る．

変数互換の列で表し，最後にそれらを結合して新たな現段階では，非出現制約集合 ∇ を入力とし，∇ に対

アトム変数置換 π ′ を作り π と置き換えることで，こして 1 を行う関数 smpN の実装と動作確認が終了しのルールを実現した．このとき π ′ の関数としての振ている．

る舞いは π と同じになっており，かつ π に含まれる

ここで，(Rew1)，(Rew2) のルール 2 について説

アトム変数互換の数は最小限になっている．

明する．アトムについての置換 τ は，定義域 dom(τ )に含まれる任意のアトムについて，τ を適用し，適4. 2 実行例

用後のアトムにまた τ を適用し， ... と τ 自身の以下では，実装を行った関数 simpN の入出力例を

適用先のアトムを辿っていくと，その道筋は循環示す．simpN は非出現制約集合 ∇ を入力とし，∇ にし，最終的に必ず元のアトムにたどり着く．例えば

対して (Rew1)，(Rew2)，(Simp) を出力が変化しな(a b)(a c)(b c)(a b) という置換の関数としての振くなるまで繰り返し適用して，適用後の非出現制約集

る舞いは {a ↦ b, b ↦ c, c ↦ a} であり，a から順合 ∇′ を出力する．このとき，同時に (FreshnessFial)にこの置換を適用した先のアトムを辿っていくと，も繰り返し適用し，FreshnessFail の例外が返ってきa → b → c → a → ... と循環する．この循環は一つた場合は即座に処理を中止する．

の置換につき一つとは限らず，二つ以上に分かれる

実装上の表記には，これまでの表記と異なる点があこともある．例えば (a b)(b c)(c d)(b d) の関数としることに注意する．アトム変数はこれまで同様 A やての振る舞いは {a ↦ b, b ↦ a, c ↦ d, d ↦ c} となり，B で表すが，変数は<S>のように<>で囲む．保留アト

(入力)

(入力)
X#(A B) (C D)(C A)(C A)(A B)Y;X#(A B)(A C)(B C)(A B)Y;
A#B;

A#C;

A#C;

A#D;

B#C;

B#C;

(出力)

B#D;

X#(A C)(A B)Y;

(出力)

A#B;

X#(C D)Y;

A#C;

A#C;

B#C;

A#D;
B#C;

(入力)

B#D;

A#((B C)D E)(B C)D;
図6

simpN 関数の入出力例

(出力)
A#E;

ム変数や保留変数は ⋅ を使わず (A B)C や (A B)<S>のように表記する．またアトム変数置換が空列 ∅ と(入力)

なっている保留アトム変数 ∅ ⋅ A や変数 ∅ ⋅ S は，空列

A#\(D E)(B C)(F G)H. <S>;

∅ を省略して A や<S>と表記する．関数記号はこれまA#B;

で同様 f や g で表すが，関数適用式は f A (B C)<S>

A#C;のように，関数記号の後ろに引数式を空白で区切って

B#D;

書く．ラムダ式は λ を\で表す．例えば λ∅ ⋅ A.∅ ⋅ S

B#E;

は\A.<S>となる．

C#D;

図 6 に simpN の入出力例を示す．図 6 の入力と出C#E;

力はともに非出現制約集合を表しており，集合に含ま(出力)れている各非出現制約が; で区切られて並んでいる．

A#\(D E)(F G)H. (B C)<S>;

この例は [5](Example 4.3) を実行した例であり，正しA#B;

く動作していることが分かる．

A#C;

以下に他の三つの実行例も示す．一つ目は前節B#D;で述べた (Rew1)，(Rew2) のルール 2 の実行例で

B#E;ある．想定通りに動作している．二つ目は (Rew1)，

C#D;(Rew2) のルール 3 の実行例である．アトム変数置

C#E;

換 ((∅ ⋅ B ∅ ⋅ C) ⋅ D ∅ ⋅ E) が右側の保留アトム変数(∅ ⋅ B ∅ ⋅ C) ⋅ D に適用され，保留アトム変数 ∅ ⋅ E

5 まとめに置き換わっている．三つ目は (Simp) のルール 7-b

本稿では，アトム変数を用いた名目単一化アルゴリの実行例である．左辺のアトム変数 A と関係のない

ズムの実装に向けて，その取り組みを報告した． [5]

右辺のラムダの直後の保留アトム変数に含まれるアで提案された推論規則に基づいて，それらの構文や規トム変数置換 (∅ ⋅ B ∅ ⋅ C) が，ラムダの直後の保留

則のより実装に適した形への再定義や，新たな規則のアトム変数の中から削除され，ラムダ式の中の保留変導入を行い，その手続きの一部を実装した．

数 ∅⋅ < S > に適用されている．

今後の課題としては，AVSOL NABLA の残りの規則

の実装と，その後の AVNOM UNIFY の実装が挙げられる．
謝辞 本研究の一部は JSPS 科研費 JP18K11233,

JP19K11891, JP19K11893 の助成を受けて行われた．
参 考 文 献[ 1 ] Gabbay, M.J., Pitts, A.M.: A new approach toabstract syntax with variable binding. Formal Aspects Comput. 13, 341–363 (2002)[ 2 ] Kikuchi, K., Aoto, T.: Conﬂuence and commutation for nominal rewriting systems with atomvariables. In: Proceedings of the 30th LOPSTR.

LNCS, vol. 12561, pp. 56–73. Springer-Verlag (2021)[ 3 ] Kutz, Y., Schmidt-Schauß, M.: Rewriting withgeneralized nominal uniﬁcation. Math. Struct. Comput. Sci. 30, 710–735 (2020)[ 4 ] Pitts, A.M.: Nominal logic, a ﬁrst order theoryof names and binding. Inform. Comput. 186, 165–
193 (2003)[ 5 ] Schmidt-Schauß, M., Sabel, D., Kutz, Y.D.K.:
Nominal uniﬁcation with atom-variables. J. Symb.
Comput. 90, 42–64 (2019)[ 6 ] Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal
uniﬁcation. In: Proceedings of the 17th CSL. LNCS,
vol. 2803, pp. 513–527. Springer-Verlag (2003)[ 7 ] Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal uniﬁcation. Theoret. Comput. Sci. 323, 473–497(2004)