前の記事：一階述語論理をPythonで組み立てる：論理式の構文木と自由変数
一階述語論理では、論理式の中に現れる変数へ項を代入します。例えば、$P(x)$ に $y$ を代入すると $P(y)$ になります。
しかし、量化記号を含む式では、単純な文字列置換は使えません。置換した項に含まれる変数が、量化記号によって意図せず束縛されることがあるためです。
この記事では、構文木として表現した一階述語論理の論理式に対して、次を実装します。
- 項の代入
- 論理式への代入
- 変数捕獲を避けるα変換
- 全称閉包
自由変数への代入
論理式 $\alpha(x)$ において自由に現れる $x$ を項 $t$ へ置き換える操作を、次のように表します。
\alpha(x \mapsto t)
例えば、$P(x, y)$ に $x$ へ $f(z)$ を代入すると、$P(f(z), y)$ になります。置換後の自由変数には、もともと自由だった変数に加えて、代入した項の自由変数も現れます。
項を置換する
構文木の記事で定義した Term に対して、対象の変数名と置換後の項を受け取る関数を定義します。
substitution.py
from __future__ import annotations
from formulas import (
Conjunction,
Disjunction,
Equality,
Equivalence,
Exists,
Falsum,
Formula,
Forall,
Implication,
Negation,
PredicateApplication,
Verum,
)
from alpha_conversion import rename_bound
from fresh_variable import fresh_variable
from terms import Constant, FunctionApplication, Term, Variable
def substitute_term(term: Term, variable: str, replacement: Term) -> Term:
if isinstance(term, Variable):
return replacement if term.name == variable else term
if isinstance(term, Constant):
return term
if isinstance(term, FunctionApplication):
return FunctionApplication(
term.name,
tuple(
substitute_term(argument, variable, replacement)
for argument in term.arguments
),
)
raise TypeError(f"unknown term: {term!r}")
def substitute(
formula: Formula,
variable: str,
replacement: Term,
) -> Formula:
if isinstance(formula, (Verum, Falsum)):
return formula
if isinstance(formula, PredicateApplication):
return PredicateApplication(
formula.name,
tuple(
substitute_term(argument, variable, replacement)
for argument in formula.arguments
),
)
if isinstance(formula, Equality):
return Equality(
substitute_term(formula.left, variable, replacement),
substitute_term(formula.right, variable, replacement),
)
if isinstance(formula, Negation):
return Negation(substitute(formula.formula, variable, replacement))
if isinstance(formula, Conjunction):
return Conjunction(
substitute(formula.left, variable, replacement),
substitute(formula.right, variable, replacement),
)
if isinstance(formula, Disjunction):
return Disjunction(
substitute(formula.left, variable, replacement),
substitute(formula.right, variable, replacement),
)
if isinstance(formula, Implication):
return Implication(
substitute(formula.left, variable, replacement),
substitute(formula.right, variable, replacement),
)
if isinstance(formula, Equivalence):
return Equivalence(
substitute(formula.left, variable, replacement),
substitute(formula.right, variable, replacement),
)
if isinstance(formula, Forall):
if formula.variable.name == variable:
return formula
if formula.variable.name in replacement.free_variables():
fresh = fresh_variable(formula.formula, replacement)
renamed = rename_bound(
formula.formula,
formula.variable.name,
fresh.name,
)
return Forall(
fresh,
substitute(renamed, variable, replacement),
)
return Forall(
formula.variable,
substitute(formula.formula, variable, replacement),
)
if isinstance(formula, Exists):
if formula.variable.name == variable:
return formula
if formula.variable.name in replacement.free_variables():
fresh = fresh_variable(formula.formula, replacement)
renamed = rename_bound(
formula.formula,
formula.variable.name,
fresh.name,
)
return Exists(
fresh,
substitute(renamed, variable, replacement),
)
return Exists(
formula.variable,
substitute(formula.formula, variable, replacement),
)
raise TypeError(f"unknown formula: {formula!r}")
量化変数が置換対象と同じ場合、その量化記号の内側では対象変数が自由に現れていません。そのため、量化式の内側へは代入しません。
変数捕獲
次の式を考えます。
\forall y\,R(x, y)
ここで $x$ へ $y$ を単純に代入すると、$\forall y\,R(y, y)$ になります。しかし、代入した $y$ まで外側の $\forall y$ に束縛されてしまいます。
この現象を変数捕獲と呼びます。元の式で自由だった $x$ に項 $y$ を代入したのに、結果ではその $y$ が束縛変数として扱われています。
変数捕獲を避けるには、先に束縛変数 $y$ を別名へ変更します。
\forall z\,R(x, z)
その後で $x$ へ $y$ を代入すると、$\forall z\,R(y, z)$ になります。
束縛変数をα変換する
量化式の束縛変数を、別の変数名へ変更する関数を実装します。内側に同じ変数名の量化がある場合は、そこで外側の束縛が隠れるため、内側へは変更を伝えません。
alpha_conversion.py
from __future__ import annotations
from formulas import (
Conjunction,
Disjunction,
Equality,
Equivalence,
Exists,
Falsum,
Formula,
Forall,
Implication,
Negation,
PredicateApplication,
Verum,
)
from terms import Constant, FunctionApplication, Term, Variable
def rename_term(term: Term, old: str, new: str) -> Term:
if isinstance(term, Variable):
return Variable(new) if term.name == old else term
if isinstance(term, Constant):
return term
if isinstance(term, FunctionApplication):
return FunctionApplication(
term.name,
tuple(rename_term(argument, old, new) for argument in term.arguments),
)
raise TypeError(f"unknown term: {term!r}")
def rename_bound(formula: Formula, old: str, new: str) -> Formula:
if isinstance(formula, (Verum, Falsum)):
return formula
if isinstance(formula, PredicateApplication):
return PredicateApplication(
formula.name,
tuple(rename_term(argument, old, new) for argument in formula.arguments),
)
if isinstance(formula, Equality):
return Equality(
rename_term(formula.left, old, new),
rename_term(formula.right, old, new),
)
if isinstance(formula, Negation):
return Negation(rename_bound(formula.formula, old, new))
if isinstance(formula, Conjunction):
return Conjunction(
rename_bound(formula.left, old, new),
rename_bound(formula.right, old, new),
)
if isinstance(formula, Disjunction):
return Disjunction(
rename_bound(formula.left, old, new),
rename_bound(formula.right, old, new),
)
if isinstance(formula, Implication):
return Implication(
rename_bound(formula.left, old, new),
rename_bound(formula.right, old, new),
)
if isinstance(formula, Equivalence):
return Equivalence(
rename_bound(formula.left, old, new),
rename_bound(formula.right, old, new),
)
if isinstance(formula, Forall):
if formula.variable.name == old:
return formula
return Forall(
formula.variable,
rename_bound(formula.formula, old, new),
)
if isinstance(formula, Exists):
if formula.variable.name == old:
return formula
return Exists(
formula.variable,
rename_bound(formula.formula, old, new),
)
raise TypeError(f"unknown formula: {formula!r}")
変数名を安全に選ぶ
α変換で使う変数名は、式や置換項にすでに現れる名前と衝突しないように選びます。
fresh_variable.py
from __future__ import annotations
from formulas import (
Conjunction,
Disjunction,
Equality,
Equivalence,
Exists,
Falsum,
Formula,
Forall,
Implication,
Negation,
PredicateApplication,
Verum,
)
from terms import Constant, FunctionApplication, Term, Variable
def variable_names_in_term(term: Term) -> set[str]:
if isinstance(term, (Variable, Constant)):
return {term.name} if isinstance(term, Variable) else set()
if isinstance(term, FunctionApplication):
return set().union(
*(variable_names_in_term(argument) for argument in term.arguments)
)
raise TypeError(f"unknown term: {term!r}")
def variable_names(formula: Formula) -> set[str]:
if isinstance(formula, (Verum, Falsum)):
return set()
if isinstance(formula, PredicateApplication):
return set().union(
*(variable_names_in_term(argument) for argument in formula.arguments)
)
if isinstance(formula, Equality):
return variable_names_in_term(formula.left) | variable_names_in_term(formula.right)
if isinstance(formula, Negation):
return variable_names(formula.formula)
if isinstance(formula, (Conjunction, Disjunction, Implication, Equivalence)):
return variable_names(formula.left) | variable_names(formula.right)
if isinstance(formula, (Forall, Exists)):
return {formula.variable.name} | variable_names(formula.formula)
raise TypeError(f"unknown formula: {formula!r}")
def fresh_variable(formula: Formula, replacement: Term) -> Variable:
used = variable_names(formula) | variable_names_in_term(replacement)
index = 0
while (candidate := f"v{index}") in used:
index += 1
return Variable(candidate)
実際の substitute() では、量化変数が置換項の自由変数に含まれている場合に fresh_variable() と rename_bound() を組み合わせます。
capture_avoiding.py
from substitution import substitute
from formulas import Formula
from terms import Term
def capture_avoiding_substitute(
formula: Formula,
variable: str,
replacement: Term,
) -> Formula:
return substitute(formula, variable, replacement)
例えば、$\forall y\,R(x, y)$ の自由変数 $x$ へ $y$ を代入します。置換項 $y$ が既存の束縛変数と衝突するため、先に束縛変数を新しい $v0$ へα変換します。
capture_example.py
from capture_avoiding import capture_avoiding_substitute
from formulas import Forall, PredicateApplication
from terms import Variable
x = Variable("x")
y = Variable("y")
formula = Forall(y, PredicateApplication("R", (x, y)))
result = capture_avoiding_substitute(formula, "x", y)
print(formula)
print(sorted(formula.free_variables()))
print(result)
print(sorted(result.free_variables()))
∀y. R(x, y)
['x']
∀v0. R(y, v0)
['y']
全称閉包
自由変数をすべて全称量化して得られる文を、元の論理式の全称閉包と呼びます。
\alpha(x_0, \ldots, x_n)
\quad\longmapsto\quad
\forall x_0\cdots\forall x_n\,\alpha
universal_closure.py
from formulas import Formula, Forall
from terms import Variable
def universal_closure(formula: Formula) -> Formula:
result = formula
for name in reversed(sorted(formula.free_variables())):
result = Forall(Variable(name), result)
return result
例えば、$P(x) \to Q(y)$ の全称閉包を出力します。
from formulas import Implication, PredicateApplication
from terms import Variable
x = Variable("x")
y = Variable("y")
formula = Implication(
PredicateApplication("P", (x,)),
PredicateApplication("Q", (y,)),
)
closed_formula = universal_closure(formula)
print(formula)
print(sorted(formula.free_variables()))
print(closed_formula)
print(sorted(closed_formula.free_variables()))
(P(x) → Q(y))
['x', 'y']
∀x. ∀y. (P(x) → Q(y))
[]
論理公理との関係
代入と全称閉包は、量化記号を含む論理公理を扱うために必要です。例えば、普遍例化に対応する公理スキーマは、項 $t$ が代入可能なときの
\forall x\,\alpha \to \alpha(x \mapsto t)
です。変数捕獲を避ける条件を無視すると、異なる意味の論理式を公理として生成してしまいます。
このため、論理公理スキーマの実装は、単なる文字列テンプレートの展開ではありません。構文木、自由変数、α変換、置換を組み合わせる必要があります。
まとめ
一階述語論理の代入を実装するには、次の処理が必要です。
- 項と論理式を再帰的にたどる
- 量化変数と置換対象が同じ場合は、量化子の内側へ入らない
- 置換項の自由変数が量化変数と衝突する場合はα変換する
- 自由変数を全称量化して全称閉包を作る
これらは、量化を含む論理公理スキーマや形式的証明を実装するための基盤になります。次の記事では、論理公理と $\Sigma$-公理系にこれらの処理を組み込みます。