"∀" や "∃" のある論理式を、リストを処理するコードで表して読解

例えば以下のような論理式がある。（Wikipediaのε-δ論法より）

{}^{\forall} \varepsilon > 0, \; {}^{\exists} \delta > 0 \;;\; {}^{\forall} x \in \mathbb{R} \; \left[ 0 < \left| x - a \right| < \delta \Rightarrow \left| f(x) - b \right| < \varepsilon \right]

これが何を主張しているかなどは置いておいて、量化子「∀」や「∃」がいくつも登場してどう読み取ればいいのか掴みにくい。日本語で書かれた場合も、「任意の〜について」「ある〜が存在して」「全ての〜に対して」となかなか厄介。式が頭に入ってこないのは理論を理解する以前の問題でとてもつらい。

読み取れるかどうかは恐らく慣れの問題だが、であればコードを書き慣れている人間ならコードで表したほうが読みやすいのではないかと思った。というわけで試してみる。

コードに翻訳

これをRubyのコードでそれっぽく表すと以下のようになる。このコードはまともには動かないので実行することはできないが、ひとまず個人的には式がとっつきやすくなった。

• 量化の入れ子の様子がわかりやすく、ひとつずつ順番に考えられる
• 単体試験を書いたりする要領で、境界値の扱いなど細かいところまで目が届きやすい

# x → a のとき f(x) → b となるか判定する
def converges?(f, a, b)
	POSITIVE_NUMBERS.all? do |e|
		POSITIVE_NUMBERS.any? do |d|
			REAL_NUMBERS.all? do |x|
				if 0 < (x - a).abs && (x - a).abs < d
					(f.call(x) - b).abs < e
				else
					true
				end
			end
		end
	end
end

コードへの書き換えは機械的。単に以下のようにしている。

• 全称量化「∀x」 → enum.all? { |x| prop(x) }
• 存在量化「∃x」 → enum.any? { |x| prop(x) }
  • 「実数全体を無限リスト化」は本来できないので、enumというのはあくまでイメージ
• 論理包含「⇒」 → prop1(x) ? prop2(x) : true
  • 左側の条件を満たさないときは真とすることに注意

論理包含はこの性質により、全称量化の対象範囲を事前に絞り込むという捉え方もできる。コードに反映すると以下の通り、 filter したものを all? で評価すればいい。

def converges?(f, a, b)
	POSITIVE_NUMBERS.all? do |e|
		POSITIVE_NUMBERS.any? do |d|
			REAL_NUMBERS.filter do |x|
				0 < (x - a).abs && (x - a).abs < d
			end.all? do |x|
				(f.call(x) - b).abs < e
			end
		end
	end
end

※ もっとしっかり考えるなら、 prop(x) が例外を投げる（暗黙の前提条件を満たしていない）ときも偽と扱うべきかもしれない。（ prop(x) rescue false ）

他の言語の場合

リストを扱うメソッドや関数があるなら、だいたい同様のものがある。

• Java: Stream の allMatch や anyMatch
  • ドキュメントにも「全称量化」「存在量化」の語句がある
• JavaScript: Array の every や some
• Python: 組み込み関数の all や any

※ 再度になるが、「実数全体を無限リスト化」は本来できないので、これらはあくまでイメージとして挙げている。

おまけ：冒頭の式の意味や利用

例に挙げた論理式は、関数の極限（収束）について述べている。以下の式と等価であり、しかも「無限に近づける」といった曖昧な表現をなくしているため、厳密な定義として使える。（無限の概念はとにかく落とし穴が多く、雑に扱うといずれ間違える）

\lim_{x \to a} f(x) = b

0 < (x - a).abs という条件を入れているため、常に x != a であることが保証される。そのため収束を考えるだけなら f(a) 自体はどうなっていても構わない（ b と異なる値でも未定義でもゼロ除算でもOK）。

（ x = a での）関数の連続性は、コードで表すと以下のように判定できる。 f(a) も計算できることが条件に入り、メソッドを展開する場合は 0 < (x - a).abs という条件を取っても構わない。

def continuous?(f, a)
	converges?(f, a, f.call(a))
end