C# で演算子を実装する (5)

前回の記事では、キャスト演算子、インデクサーなどについて説明しました。
今回は論理演算子を扱います。

ユーザー定義型で直接オーバーロードできる論理演算子には、!, &, ^, | さらに true および false 演算子があります。
ただし整数型においては、&, ^, | はビット演算を表します。
また、否定 ! は、整数のビット演算においては補数 ~ に相当します。

論理演算については、bool 型や bool? 型の状態で扱えば実務上は事足りることが多く、ユーザー定義型でこれらの演算子をオーバーロードして使う機会はあまりないと思います。
そこで、今回は && および || 演算子による短絡評価 (ショート サーキット) を検証してみました。

短絡評価 (ショート サーキット)

ユーザー定義型で && および || 演算子による短絡評価を利用するには、次の条件を満たす必要があります。

  • & および | について、2つの引数と戻り値の型はすべて、定義元の型
  • true および false 演算子が宣言されている

そしてこのとき、x && y は x が偽を表すならば y には何もせず x を返し、そうでなければ x & y を評価します。
形式的に書くと T.false(x) ? x : (x & y) のようになります。
同様に、x || y は x が真を表すならば y には何もせず x を返し、そうでなければ x | y を評価します。
形式的に書くと T.true(x) ? x : (x | y) のようになります。

bool 型における短絡評価も上記の法則に従っていると見なすことができ、短絡評価の概念を bool 型以外に拡張したことになります。
なお、bool? 型では && および || 演算子を利用できません。

さて、上記の仕組みから考えると、短絡評価を適用できる論理体系とは、x と y のうち1つ以上が偽を表すのであれば x & y も偽を表し、x と y のうち1つ以上が真を表すのであれば x | y も真を表すものである必要があります。
これは、真・偽のほかに第3の値の存在を考える3値論理で体系を構成する場合、クリーネの3値論理に相当します。
bool? 型における論理演算 (!, &, ^, |) もこのクリーネの3値論理に従います。
3値論理については記事の後半で補足します。

実装例

今回の実装例では、与えられた文字列が真を表すのか、偽を表すのか、それ以外かの3値を判定する構造体を作成し、各論理演算子をオーバーロードしています。
以下にソースコードを示します。

namespace OperatorsLib.Structs
{
public struct StringBool
{
public static StringBool True { get; } = bool.TrueString;
public static StringBool False { get; } = bool.FalseString;
public static StringBool Unknown { get; } = null;
// bool? として持つこともできますが、この例ではあえて論理演算を自作します。
public string Value { get; }
public bool IsTrue => bool.TryParse(Value, out var b) && b;
public bool IsFalse => bool.TryParse(Value, out var b) && !b;
public bool IsUnknown => !bool.TryParse(Value, out var _);
public StringBool(string value) => Value = value;
public override string ToString() => Value ?? "Unknown";
public static implicit operator StringBool(string v) => new StringBool(v);
public static explicit operator bool?(StringBool v) => v.IsUnknown ? default(bool?) : v.IsTrue;
public static bool operator true(StringBool v) => v.IsTrue;
public static bool operator false(StringBool v) => v.IsFalse;
public static StringBool operator !(StringBool v) => v.IsUnknown ? Unknown : v.IsTrue ? False : True;
public static StringBool operator &(StringBool v1, StringBool v2) => v1.IsFalse || v2.IsFalse ? False : v1.IsUnknown || v2.IsUnknown ? Unknown : True;
public static StringBool operator ^(StringBool v1, StringBool v2) => v1.IsUnknown || v2.IsUnknown ? Unknown : v1.IsTrue ^ v2.IsTrue ? True : False;
public static StringBool operator |(StringBool v1, StringBool v2) => v1.IsTrue || v2.IsTrue ? True : v1.IsUnknown || v2.IsUnknown ? Unknown : False;
}
}
view raw StringBool.cs hosted with ❤ by GitHub

コンストラクターの処理で bool? に変換することもできますが、この例ではあえて Value プロパティで入力の文字列を保持することとし、論理演算を自作しています。上記のように実装することで、下記のコードのように短絡評価を使えるようになります。

[TestMethod]
public void Tables()
{
StringBool t = "true";
StringBool n = "force";
StringBool f = "false";
var s = new[] { t, n, f };
// 真理値表を作成します。
for (int i = 0; i < 3; i++)
{
for (int j = 0; j < 3; j++)
{
Console.Write($"{s[i] && s[j],-8}");
}
Console.WriteLine();
}
Console.WriteLine();
for (int i = 0; i < 3; i++)
{
for (int j = 0; j < 3; j++)
{
Console.Write($"{s[i] || s[j],-8}");
}
Console.WriteLine();
}
}
view raw StringBoolTest.cs hosted with ❤ by GitHub

このコードにより、下図のような真理値表が得られます。
短絡になったケースは小文字始まりで表示されています。

StringBool-Tables

クリーネの3値論理

情報技術で多く使われているクリーネの3値論理における、真でも偽でもない3つ目の値 (C# では bool? 型の null) とは、「真でも偽でもない、もう一つの異なる固定値」ではなく「本来は真または偽の値を持つが、現在はわかっていない状態」と考えたほうが意味論的には理解しやすいと思います。
(命題論理の考え方については、以前に命題論理を実装する (C#) という記事で書きました。)

そこで、null の代わりに unknown という名前を使うことにします。
具体例として、unknown & false は、左側のオペランドが実際に true とわかっても false とわかっても式全体では false であることが確定しています。また、unknown & true は、左側のオペランドが true とわかるか false とわかるかで式全体の結果が変わるため現在は unknown です。すると、x & y が現時点で true と確定するのは x と y がともに true のときだけです。
残りの !, ^, | についても同様に考えて体系を構成できます。

bool? 型における論理演算もこれと同じになります。
演算結果の真理値表はなかなか丸暗記できないと思いますが、上記のように短絡評価と関連付けることで導けるようになるはずです。

また、== および != 演算子を等価性ではなく命題論理における同値性として扱いたい場合、これらの演算子の戻り値の型を bool ではなく定義元の型とし、x == y!(x ^ y) と同じ意味に、x != yx ^ y と同じ意味になるようにオーバーロードします。

もし null を unknown ではなく「もう一つの異なる固定値」と考えて「一方が null ならば x & y は null」のような体系を立てる場合であっても、各論理演算子をオーバーロードすれば実現できるでしょう。ただし、短絡評価はできません。

制御条件式

true 演算子が宣言されていることで、if ステートメントなどにおける制御条件式として if (obj) のように使えます。
また、true 演算子の代わりに bool 型への暗黙的型変換を宣言することででも、制御条件式として使えるようになります。
両方を宣言した場合は、この暗黙的型変換が優先されるようです。

public static implicit operator bool(StringBool v) => v.IsTrue;

次回はその他の注意点や設計についてです。

前回: C# で演算子を実装する (4)
次回: C# で演算子を実装する (6)

作成したサンプル

バージョン情報

  • C# 8.0
  • .NET Standard 2.1
  • .NET Core 3.1

参照

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

// この投稿は 数学 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_Xp の真偽性は等しいということになり、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#)

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

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

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

Raymond Smullyan「記号論理学: 一般化と記号化」
「記号論理学: 一般化と記号化」
高橋 昌一郎, 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

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

PropositionsConsole

 

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

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

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

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

バージョン情報
.NET Framework 4.5

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