命題論理を実装する (C#)

// この投稿は 数学 Advent Calendar 2016 の 16 日目の記事です。

命題といえば高校数学で「かつ」「または」「ならば」などを学習すると思いますが、
この投稿では、これらを一般化、形式化した命題論理をプログラミングで表現することを目指します。
プログラミングをしない方も、適宜飛ばせばなんとか読めると思います。

用語や定義については、主に Raymond Smullyan「記号論理学: 一般化と記号化」の第 7 章「命題論理入門」に記載されているものを使い、
解説と実装をしていきます。
プログラミング言語としては C# (.NET) を利用します。

「記号論理学: 一般化と記号化」
高橋 昌一郎, Raymond Smullyan, 川辺 治之

 

論理結合子

任意の命題 p は、真偽値 (truth value) を持ちます。真偽値とは、真 (T) または偽 (F) です。
そして、「かつ」「または」「ならば」などを一般化した概念を論理結合子 (logical connective) と呼び、次のものがあります。

1. 否定 (～p)
   真偽値を反転させます。
2. 論理積 (p ∧ q)
   p および q がともに真のときに限り真です。
3. 論理和 (p ∨ q)
   p または q のうち、少なくとも一方が真のときに真です。
4. 含意 (p ⇒ q)
   ～p ∨ q と同義です。
5. 同値 (p ≡ q)
   (p ⇒ q) ∧ (q ⇒ p) と同義です。計算機においては、XOR 演算の否定と同義です。

論理式

さらに、論理式を次のように定義します。

• 命題変数 (propositional variable): 命題を表す変数。値は、真または偽となりうる。
• 命題定数 (propositional constant): 真を表す t および偽を表す f。
• 論理式 (formula): 命題変数、命題定数、論理結合子により構成される式。

ここまでの内容をもとに、論理式を実装します。 論理結合子は、否定のみが単項で、他はすべて二項です。

	using System;
	using System.Diagnostics;
	namespace Blaze.Propositions
	{
	[DebuggerDisplay(@"\{{ToString()}: {TruthValue}\}")]
	public abstract class Formula
	{
	internal static Formula[] EmptyFormulas { get; } = new Formula[0];
	public abstract Formula[] Children { get; }
	public abstract bool? TruthValue { get; }
	}
	public abstract class VariableFormula : Formula
	{
	public override Formula[] Children => EmptyFormulas;
	public override bool? TruthValue => Value;
	public bool? Value { get; set; }
	}
	public class VariableFormula<TStatement> : VariableFormula
	{
	public TStatement Statement { get; }
	public VariableFormula(TStatement statement)
	{
	Statement = statement;
	}
	public override string ToString() => $"{Statement}";
	}
	public class ConstantFormula : Formula
	{
	public override Formula[] Children => EmptyFormulas;
	public override bool? TruthValue => Value;
	public bool Value { get; }
	public ConstantFormula(bool value)
	{
	Value = value;
	}
	public override string ToString() => Value ? "t" : "f";
	}
	public abstract class UnaryFormula : Formula
	{
	public override Formula[] Children { get; }
	public Formula Operand { get; }
	protected UnaryFormula(Formula operand)
	{
	Operand = operand;
	Children = new[] { Operand };
	}
	}
	public abstract class BinaryFormula : Formula
	{
	public override Formula[] Children { get; }
	public Formula Operand1 { get; }
	public Formula Operand2 { get; }
	protected BinaryFormula(Formula operand1, Formula operand2)
	{
	Operand1 = operand1;
	Operand2 = operand2;
	Children = new[] { Operand1, Operand2 };
	}
	}
	public class NegationFormula : UnaryFormula
	{
	public override bool? TruthValue => !Operand.TruthValue;
	public NegationFormula(Formula operand) : base(operand) { }
	public override string ToString() => $"～({Operand})";
	}
	public class AndFormula : BinaryFormula
	{
	public override bool? TruthValue => Operand1.TruthValue & Operand2.TruthValue;
	public AndFormula(Formula operand1, Formula operand2) : base(operand1, operand2) { }
	public override string ToString() => $"({Operand1})∧({Operand2})";
	}
	public class OrFormula : BinaryFormula
	{
	public override bool? TruthValue => Operand1.TruthValue | Operand2.TruthValue;
	public OrFormula(Formula operand1, Formula operand2) : base(operand1, operand2) { }
	public override string ToString() => $"({Operand1})∨({Operand2})";
	}
	public class ImplicationFormula : BinaryFormula
	{
	public override bool? TruthValue => !Operand1.TruthValue | Operand2.TruthValue;
	public ImplicationFormula(Formula operand1, Formula operand2) : base(operand1, operand2) { }
	public override string ToString() => $"({Operand1})⇒({Operand2})";
	}
	public class EquivalenceFormula : BinaryFormula
	{
	public override bool? TruthValue => !(Operand1.TruthValue ^ Operand2.TruthValue);
	public EquivalenceFormula(Formula operand1, Formula operand2) : base(operand1, operand2) { }
	public override string ToString() => $"({Operand1})≡({Operand2})";
	}
	}

view raw Formula.cs hosted with ❤ by GitHub

式を簡単に記述できるようにするため、静的メソッドを用意します。

	namespace Blaze.Propositions
	{
	public abstract class Formula
	{
	// (中略)
	public static Formula True { get; } = new ConstantFormula(true);
	public static Formula False { get; } = new ConstantFormula(false);
	public static VariableFormula<TStatement> Variable<TStatement>(TStatement statement) => new VariableFormula<TStatement>(statement);
	public static Formula Imply(Formula v1, Formula v2) => new ImplicationFormula(v1, v2);
	public static Formula Equivalent(Formula v1, Formula v2) => new EquivalenceFormula(v1, v2);
	public static Formula operator !(Formula v) => new NegationFormula(v);
	public static Formula operator &(Formula v1, Formula v2) => new AndFormula(v1, v2);
	public static Formula operator |(Formula v1, Formula v2) => new OrFormula(v1, v2);
	}
	}

view raw Formula.cs hosted with ❤ by GitHub

 

恒真式および矛盾

論理式のうち、含まれる命題変数がどのような真偽値の組合せになっても真であるものを恒真式 (tautology) と呼びます。
逆に、含まれる命題変数がどのような真偽値の組合せになっても偽であるものを矛盾論理式または矛盾 (contradiction) と呼びます。
簡単な例を挙げると、p ∨ ～p は恒真式で、p ∧ ～p は矛盾です。

論理式が恒真式あるいは矛盾であるかどうかを判定するためのメソッドは、次のように実装できます。

	using System;
	using System.Collections.Generic;
	using System.Linq;
	namespace Blaze.Propositions
	{
	public abstract class Formula
	{
	// (中略)
	// GetDescendants メソッドでは、要素が重複する可能性があります。
	public IEnumerable<Formula> GetDescendants() => new[] { this }.Concat(Children.SelectMany(f => f.GetDescendants()));
	public VariableFormula[] GetVariables() => GetDescendants().OfType<VariableFormula>().Distinct().Where(v => v.Value == null).ToArray();
	static readonly bool[] bools = new[] { true, false };
	static readonly IEnumerable<bool> initialCombinations = new[] { false };
	public bool IsTautology()
	{
	var variables = GetVariables();
	try
	{
	// 変数の値のすべての組合せを列挙します。
	return variables
	.Aggregate(initialCombinations, (q, v) => q.SelectMany(_ => bools.Select(b => { v.Value = b; return _; })))
	.All(_ => TruthValue.Value);
	}
	finally
	{
	foreach (var v in variables)
	v.Value = null;
	}
	}
	public bool IsContradiction() => (!this).IsTautology();
	}
	}

view raw Formula.cs hosted with ❤ by GitHub

以上のコードをまとめて、Blaze (GitHub) というライブラリとして公開しています。 NuGet でインストールできます。

 

ライブラリを使ってみる

さて、このライブラリを利用すると、命題論理に関する定理を証明できるようになります。
実際にいくつかやってみましょう。
Visual Studio で新規のコンソール アプリケーション プロジェクトを作成して、NuGet で Blaze をインストールします。
そして次のようなコードを記述します。

	using System;
	using Blaze.Propositions;
	using static System.Console;
	using static Blaze.Propositions.Formula;
	namespace PropositionsConsole
	{
	class Program
	{
	static void Main(string[] args)
	{
	var p = Variable("P");
	var q = Variable("Q");
	var r = Variable("R");
	TestContradiction(p & !p);
	TestTautology(p | !p);
	TestTautology(Imply(p, !p));
	TestContradiction(Imply(p, !p));
	TestContradiction(Equivalent(p, !p));
	WriteLine();
	TestTautology(Equivalent(!(p & q), !p | !q));
	TestTautology(Equivalent(!(p | q), !p & !q));
	WriteLine();
	TestTautology(Imply(Imply(p, q), Imply(q, p)));
	TestContradiction(Imply(Imply(p, q), Imply(q, p)));
	TestTautology(Imply(p & Imply(p, q), q));
	WriteLine();
	WriteLine("三段論法：");
	TestTautology(Imply(Imply(p, q) & Imply(q, r), Imply(p, r)));
	WriteLine("背理法：");
	TestTautology(Imply(Imply(p, q) & Imply(p, !q), !p));
	WriteLine("対偶：");
	TestTautology(Equivalent(Imply(p, q), Imply(!q, !p)));
	WriteLine();
	}
	static void TestTautology(Formula f)
	{
	WriteLine($"{f} is{(f.IsTautology() ? "" : " not")} a tautology.");
	}
	static void TestContradiction(Formula f)
	{
	WriteLine($"{f} is{(f.IsContradiction() ? "" : " not")} a contradiction.");
	}
	}
	}

view raw Program.cs hosted with ❤ by GitHub

恒真式であるということは、その論理式がつねに成り立つということです。
このコードを実行することで、三段論法、背理法、対偶などを証明できます。

 

次回は、このライブラリを利用してもう少し高度な問題を解いてみます。

次回: 命題論理の複雑な問題を解く (C#)

作成したライブラリ
Blaze (GitHub)
Blaze (NuGet Gallery)

作成したサンプル
PropositionsConsole (GitHub)

バージョン情報
.NET Framework 4.5

参照
Raymond Smullyan「記号論理学: 一般化と記号化」