Think Stitch
PRINCIPIA  最近の更新


代入の合成

構文を扱うプログラムや数学では代入(字句代入, あるいは置換, substitution)というものが出てきます. その代入の合成について考えます.

代入

まずは復習からです.代入というのは式 E の中に現れる変数 x を別の式 e で置き換えるという操作です.変数 x が出てくる(出現する)ところはすべて残さず置き換えます.これを記号で次のように書きます.

\[ E[x := e] \]

次のように書く人もいます.

\[ E[x \backslash e] \qquad E[e/x] \]

例えば次のようになります.

\[ (x \times (x + y))[x := c] = c \times (c + y) \]

代入の規則は次のとおりです:

\[ \begin{split} & x[x := e] = e \\[4pt] & y[x := e] = y \quad \cdots \quad y \neq x \\[4pt] & (E \oplus F)[x := e] = (E[x := e]) \oplus (F[x := e]) \end{split} \]

言葉で説明すると次のようになります:

  1. 変数 x は式 e に置き換えます.
  2. x と異なる変数 y は影響を受けません.
  3. 式が複数の部分式からできているときは,それぞれの部分式に対して代入を行います.

ここで記号 ⊕ は式を構成する演算子の代表として使いました.実際には + だったり,前置きの関数記号だったりします.また,変数を束縛するような構文については考えないことにします.

代入を行う変数は1つとは限りません.同時に複数の変数に対して代入を行うこともできます.

\[ (x + y)[x := a, y := b] = a + b \]

代入は"同時に"行うので,例えば次のように交換もできます.

\[ (x + y)[x := y, y := x] = y + x \]

代入の合成

代入を,変数と置き換える式のペアの集合で表すことにします.ただし,1つの変数に対するペアは2つ以上はないものとします.

\[ \sigma = \{ (x_1, e_1), (x_2, e_2), \ldots, (x_n, e_n) \} \]

式 E に代入σを適用した結果の式を次のように書くことにします.

\[ E\sigma \]

例えば次の2つの代入があるとします:

\[ \begin{split} \sigma_1 &= \{ (x, x+y) \} \\ \sigma_2 &= \{ (x, a), (y, b) \} \end{split} \]

式 E(x, y) に対してこれを順に適用すると,次のようになります.

\[ \begin{split} & (E(x, y)\sigma_1)\sigma_2 \\[4pt] = & E(x + y, y)\sigma_2 \\[4pt] = & E(a + b, b) \end{split} \]

ここで1つ疑問が浮かびます.2つの連続した代入の適用と同じ効果を持つ1つの代入はあるのでしょうか?

\[ E\sigma_1\sigma_2 = E\sigma ? \]

ここで知りたいのは特定の式 E(x, y) に対して同じ効果があるということではなく,もっと一般的に任意の式に対して同じ効果を持つ1つの代入を見つけることはできるのかということです.象徴的には次のように書くことができるでしょう.つまり代入の合成を考えるということです.

\[ \sigma_1\sigma_2 = \sigma ? \]

答えは"あります".いくつか具体的な例で考えてみると,すぐに規則を見つけることができます.式で書くと次のようになります:

\[ \sigma = \{(x, e\sigma_2)\,|\,(x, e) \in \sigma_1 \} \cup \{(x, e)\,|\,(x, e) \in \sigma_2 \land x \notin \mathrm{dom}\ \sigma_1 \} \]

合成された代入は2つの部分からなります.1つ目の部分はσ1で置き換え先となる各式 e に,先にσ2を適用してしまった代入を作るという意味です.2つ目はσ2から,σ1で置き換え対象になっている変数に対するペアを取り除いたものを表しています.したがってこの2つの部分に共通する変数はないことになります.

先ほどの例で実際に合成を作ってみると次のようになります:

\[ \begin{split} \sigma & = \{(x, (x+y)\sigma_2)\} \cup \{(y,b)\} \\[4pt] & = \{(x, a + b)\} \cup \{(y,b)\} \\[4pt] & = \{(x, a + b), (y,b) \} \end{split} \]

これを式 E(x, y) に適用すると,確かに同じ結果が得られます.

\[ \begin{split} E(x, y)\sigma & = E\{(x, a + b), (y,b) \} \\[4pt] & = E(a + b, b) \end{split} \]

構文の構成に基づく証明

本当にこの合成が正しいのかどうか不安が残るので,証明をしてみることにします.この手の問題での定石は,式の構成に対する帰納法を使うことです.

そこでまず式を帰納的に定義します.c は定数で,⊕ は先ほども書いたとおり式を構成する演算子の代表です.一般には複数ありますし,部分式も1個だったり3個以上だったりしますが,ここでは簡単のためこれだけ考えます.

\[ E ::= c \ |\ x \ | \ E \oplus E \]

代入の合成の定義を再掲しておきます.

\[ \sigma = \{(x, e\sigma_2)\,|\,(x, e) \in \sigma_1 \} \cup \{(x, e)\,|\,(x, e) \in \sigma_2 \land x \notin \mathrm{dom}\ \sigma_1 \} \]

証明したいことは任意の式 E と代入σ1, σ2について次が成り立つことです.

\[ E\sigma = E\sigma_1\sigma_2 \]

1. 定数 c の場合

これはどちらの場合も影響を受けないので自明です.

2. 変数 x の場合

変数 x の場合は σ1, σ2 それぞれに含まれているかどうかで4通りに場合分けをして考えます.

(1) 両方に含まれている場合

変数 x にσ1を適用した結果を e とします.

\[ x\sigma_1 = e \]

すると順番に適用した結果は次のようになります.

\[ x\sigma_1\sigma_2 = e\sigma_2 \]

一方,合成された代入を適用すると,定義により次のようになりますから,結果は一致します.

\[ x\sigma = e\sigma_2 \]

(2) σ1 だけに含まれている場合

先ほどと同じく,変数 x にσ1を適用した結果を e とします.

\[ x\sigma_1 = e \]

順番に適用した結果も同じです.

\[ x\sigma_1\sigma_2 = e\sigma_2 \]

合成された代入を適用した結果も同じです.この場合は(1)と同じでした.

\[ x\sigma = e\sigma_2 \]

(3) σ1 に含まれておらず σ2 には含まれている場合

まずσ1では影響を受けません.

\[ x\sigma_1 = x \]

すると順番に適用した結果は次のようになります.

\[ x\sigma_1\sigma_2 = x\sigma_2 \]

一方,合成された代入を適用すると,定義により2番目の項の対象となり,次のようになりますから,結果は一致します.

\[ x\sigma = x\sigma_2 \]

(4) どちらにも含まれていない場合

この場合は影響を受けないので自明です.

3. 式 E ⊕ F の場合

この場合は帰納法の仮定を使います.簡単な一本道です.

\[ \begin{split} & (E \oplus F)\sigma \\[4pt] = & \quad [定義] \\[4pt] & E\sigma \oplus F\sigma \\[4pt] = & \quad [帰納法の仮定] \\[4pt] & E\sigma_1\sigma_2 \oplus F\sigma_1\sigma_2 \\[4pt] = & \quad [定義] \\[4pt] & (E\sigma_1 \oplus F\sigma_1)\sigma_2 \\[4pt] = & \quad [定義] \\[4pt] & (E \oplus F)\sigma_1\sigma_2 \end{split} \]

以上で,合成が正しいことが証明できました.

Isabelle による証明

Isabelle を使って証明してみました.まず代数的データ型を使って構文を定義します.定数は省略しました.

datatype expr = Var nat | Op expr expr

次に代入を定義します.プログラムの場合は列を使うことが多いかもしれませんが,ここでは上の定義に合わせて集合にしました.そのせいで,要素をとるためにヒルベルトのイプシロンオペレータを使いました.Isabelle での記号は SOME x. P x です.述語 P を満たすある x を表します.

fun subst :: "(nat * expr) set => expr => expr" where
  "subst s (Var k) = (if k : Domain s then SOME e. (k, e) : s else (Var k))"
| "subst s (Op f e) = Op (subst s f) (subst s e)"

代入をペアの集合で表すと,1つの変数に対して複数のペアが存在できてしまうので,これを排除する条件を容易しておきます.単射(つまり関数)だということです.

definition rel_inj :: "('a * 'b) set => bool" where
  "rel_inj R = (ALL x y1 y2. (x,y1) : R & (x,y2) : R --> y1 = y2)"

証明は次のようになります.ほとんど自動でできました.

theorem "
  ALL s t. rel_inj s & rel_inj t -->
  subst t (subst s e) =
  subst ({(k, e). EX e'. (k, e') : s & e = subst t e'} Un {(k, e). (k, e) : t & k ~: Domain s}) e"
apply(unfold rel_inj_def)
apply(induct_tac e)
apply(auto)
apply(rule someI2)
apply(rule_tac x="b" in exI)
apply(simp)
apply(rule someI2)
apply(simp)
apply(blast)
apply(rule someI2)
apply(auto)
apply(rule someI2)
apply(auto)
apply(blast)
done

変数を束縛する構文がある場合を考えてみると面白いと思います.

2014/08/02
© 2013,2014,2015 PRINCIPIA Limited