12月 | 2016 | Do Design Space

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

2016年12月23日 — さかぽん

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

前回の命題論理を実装する (C#) では命題論理を扱うためのライブラリを作成しました。
今回は、このライブラリを利用して複雑な問題をいくつか解いてみます。

騎士と悪漢

まず、前回でも紹介した書籍 Raymond Smullyan「記号論理学: 一般化と記号化」から、問題を 2 つ引用します。

すべての住民は騎士または悪漢のいずれかであり、騎士はつねに本当のことを言い、悪漢はつねに噓をつく。

問題 1.3
住民 A, B がおり、A は「私たちは二人とも悪漢だ」と言った。
A, B はそれぞれ騎士か悪漢か？

問題 1.5
住民 A, B がおり、A は「私たちは同種 (二人とも騎士または二人とも悪漢のいずれか) だ」と言った。
A, B はそれぞれ騎士か悪漢か？

普通に考えて解くこともできますが、この状況を記号で表すことを考えます。
住民 X が騎士であるという命題を $k_X$ とし、X が命題 $p$ を主張したとすると、
$k_X$ と $p$ の真偽性は等しいということになり、 $k_X \equiv p$ が成り立ちます。
したがって、問題 1.3 では $k_A \equiv (\lnot k_A \land \lnot k_B)$ が、問題 1.5 では $k_A \equiv (k_A \equiv k_B)$ が成り立ちます。

前回作成したライブラリ Blaze を使って、次のように解くことができます。

      
        using System;
      
        using Blaze.Propositions;
      
        using static System.Console;
      
        using static Blaze.Propositions.Formula;
      
        namespace PropositionsConsole
      
        {
      
            class Program
      
            {
      
                static void Main(string[] args)
      
                {
      
                    Knights_1_3();
      
                    Knights_1_5();
      
                }
      
                static void Knights_1_3()
      
                {
      
                    var ka = Variable("kA");
      
                    var kb = Variable("kB");
      
                    var knowledge = Equivalent(ka, !ka & !kb);
      
                    knowledge.Determine(ka);
      
                    knowledge.Determine(kb);
      
                    WriteLine("Q 1.3");
      
                    WriteVariable(ka);
      
                    WriteVariable(kb);
      
                }
      
                static void Knights_1_5()
      
                {
      
                    var ka = Variable("kA");
      
                    var kb = Variable("kB");
      
                    var knowledge = Equivalent(ka, Equivalent(ka, kb));
      
                    knowledge.Determine(ka);
      
                    knowledge.Determine(kb);
      
                    WriteLine("Q 1.5");
      
                    WriteVariable(ka);
      
                    WriteVariable(kb);
      
                }
      
                static void WriteVariable(VariableFormula v)
      
                {
      
                    WriteLine($"{v}: {(v.Value.HasValue ? v.Value.ToString() : "Null")}");
      
                }
      
            }
      
        }

view raw Program.cs hosted with ❤ by GitHub

実行すると、問題 1.3 では A が悪漢、B が騎士と確定します。
問題 1.5 では B が騎士と確定しますが、A は確定できません。

PropositionsConsole

数当てゲーム

さて次に、David Gale「Tracking the Automatic ANT: And Other Mathematical Explorations」という書籍から、
数当てゲームを紹介します。

プレイヤーは 2 人

それぞれのプレイヤーに数が割り当てられており、自身の数を知っているが、相手の数は知らない

2 人の持つ数は、連続する 2 つの自然数 (つまり、差は 1)

ターン制で、相手の数を当てれば終了 (わかったら宣言し、わからなければ発声しない)

先攻・後攻の区別はなく、いずれが宣言してもよい

どちらのプレイヤーが何ターン目に相手の数を当てることができるか？

自分の数が 9 だとすると、与えられた条件から相手の数は 8 または 10 の 2 通りに絞られます。
ここまではすぐにわかるのですが、いずれかを確定させるには相手の将来の行動あるいは実際の行動の原因を推測する必要があります。
相手がどう考えているかを考える、という日常生活においても重要な能力を問われているようでもあります。

小さい数値でいくつか試してみましょう。
2 人のプレイヤーには対称性がありますが、ここでは大小関係を固定して、プレイヤー A が n、プレイヤー B が n+1 を持つとします。
以下では、各プレイヤーの心理状況を書くことにします。

n=1 の場合、

A「B=2 しかありえない。」
B「A=1 または A=3。A=1 ならば、A は 1 ターン目に当てるはず。A=3 ならば、A は 1 ターン目に静観するはず。」

したがって、A が 1 ターン目で当てて終了します。
n=2 の場合、

A「B=1 または B=3。B=1 ならば、B は 1 ターン目に当てるはず。B=3 ならば、B は 1 ターン目に静観するはず。」
B「A=2 または A=4。A=2 ならば、A は 2 ターン目に当てるはず (B が 1 ターン目に静観するため)。
A=4 ならば、A は 2 ターン目まで静観するはず。」

したがって、1 ターン目は両方静観し、A が 2 ターン目で当てて終了します。
このように、相手がどのように行動してくるかをあらかじめシミュレートしておけば、実際の行動に応じて相手の数を確定できることになります。

この方針でプログラミングしたものが NumberGuessConsole (GitHub) です (コードが長いため、ここには記載しません)。
このプログラムを A=8, B=9 で実行した結果です。A が 8 ターン目に当てました。
(「X @ n」は X が n ターン目に当てることを表します。)

NumberGuessConsole

各プレイヤーの脳内であらかじめシミュレーターを実行することで、値を確定させるための条件を得ます。
A の Knowledge には ((B = 7)≢(B = 9))∧((B = 7)⇒(B @ 7))∧((B = 9)⇒～(B @ 7)) と入っています。
B が 7 ターン目に静観したため、A は B=9 だとわかりました。

NumberGuessConsole

結果として、小さいほうの数 n を持つプレイヤーが n ターン目に相手の数 n+1 を当てることになります。
(プログラミングをしなくても、同様の方針により少し複雑な数学的帰納法で証明できます。)

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

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

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

素材
不気味の谷現象のイラスト (いらすとや)

バージョン情報
.NET Framework 4.5

参照
Raymond Smullyan「記号論理学: 一般化と記号化」
David Gale「Tracking the Automatic ANT: And Other Mathematical Explorations」

カテゴリー: 数学. タグ: 命題論理. 1 Comment »

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

2016年12月16日 — さかぽん

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

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

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

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

論理結合子

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

否定 (～p)
真偽値を反転させます。
論理積 (p ∧ q)
p および q がともに真のときに限り真です。
論理和 (p ∨ q)
p または q のうち、少なくとも一方が真のときに真です。
含意 (p ⇒ q)
～p ∨ q と同義です。
同値 (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「記号論理学: 一般化と記号化」

カテゴリー: プログラミング言語, 数学. タグ: 命題論理. 2 Comments »

Do Design Space

ページ

カテゴリ

タグ

ブログ PV

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

騎士と悪漢

数当てゲーム

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

論理結合子

論理式

恒真式および矛盾

ライブラリを使ってみる

最近の投稿

アーカイブ

RSS

最近のツイート

	using System;
	using Blaze.Propositions;
	using static System.Console;
	using static Blaze.Propositions.Formula;

	namespace PropositionsConsole
	{
	class Program
	{
	static void Main(string[] args)
	{
	Knights_1_3();
	Knights_1_5();
	}

	static void Knights_1_3()
	{
	var ka = Variable("kA");
	var kb = Variable("kB");

	var knowledge = Equivalent(ka, !ka & !kb);
	knowledge.Determine(ka);
	knowledge.Determine(kb);

	WriteLine("Q 1.3");
	WriteVariable(ka);
	WriteVariable(kb);
	}

	static void Knights_1_5()
	{
	var ka = Variable("kA");
	var kb = Variable("kB");

	var knowledge = Equivalent(ka, Equivalent(ka, kb));
	knowledge.Determine(ka);
	knowledge.Determine(kb);

	WriteLine("Q 1.5");
	WriteVariable(ka);
	WriteVariable(kb);
	}

	static void WriteVariable(VariableFormula v)
	{
	WriteLine($"{v}: {(v.Value.HasValue ? v.Value.ToString() : "Null")}");
	}
	}
	}

	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})";
	}
	}

	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);
	}
	}

	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();
	}
	}