はじめに

むかしむかしにスマリヤンの本を読んで以来, 作りたいと思っていた表題のプログラムを実装した記録です.

参考になった記事

そもそも perl を初めて触ったので以下のような記事が参考になりました.
perl 入門
 perl での関数の再帰的定義
[perl での文字列の置換について]
(https://tutorial.perlzemi.com/blog/20100827127859.html)

そもそも

トートロジーとは

命題の真偽に関わらず真の値を返す論理式のことです. 例えば $x$ を命題変数としたとき, $x$ が真でも偽でも, トートロジー"$x$ or not $x$" は真になります. ここで, "not" や "or" は論理関数と呼ばれます.
この例のように, 論理式は(それがトートロジーかどうかにかかわらず,) 命題変数と論理関数からなります.

論理関数とは

"and" とか "or" とか "not" とかのことです. 命題変数を引数にとります. 例えば, "$P$ and $Q$" は $P$, $Q$ が両方とも真の時のみ, 真の値をとります.
言い方を変えれば, $x$, $y$ を命題変数としたとき, and は以下のように定義されます.

\begin{align}
x~\textrm{and}~y & \equiv
\begin{cases}
\textrm{True} \quad if~(x, y) = (\textrm{True}, \textrm{True}) \\
\textrm{False} \quad if~else
\end{cases}
\end{align}

命題変数には何が入るか

命題変数には論理式か命題が入ります. 命題($P$ とか $Q$ とか)には真偽が割り当てられます. 論理式は, 論理関数と命題変数で構成されます. (命題だけの "$P$" とかも論理式です)

プログラムの大まかな流れ

まず, 論理式を作る.
- 使う命題は多くても 2 種類. ($P$ と $Q$ にしました.)
- 使う論理関数は多くても 2 種類. ("not" と "then" にしました.)
  - 重要な事実として, 全ての論理関数は "not" と "then" の組み合わせで書ける, というのがあります.
  - 定義は,

\begin{align}
\textrm{not}~x & \equiv
\begin{cases}
\textrm{True} \quad if~x = \textrm{True} \\
\textrm{False} \quad if~else
\end{cases}\\
\\
x~\textrm{then}~y & \equiv
\begin{cases}
\textrm{False} \quad if~(x, y) = (\textrm{True}, \textrm{False}) \\
\textrm{True} \quad if~else
\end{cases}
\end{align}

次に, それがトートロジーかどうか判定する.
- 例えば, "$P$ then $P$" はトートロジーです.
- 当然, "$P$ then $Q$" はトートロジーではありません.
最後に, それがトートロジーなら出力する.
- 出力したら, 論理式づくりに戻ります.

プログラムの詳細

論理式づくり

"then" と "not" を記号で代用します. "$x$ then $y$" は "($x$ > $y$)", "not $x$" は "-$x$" と書きます. 論理式は以下のように再帰的に定義された関数から出力されます.

論理式の頭に "-" ("not") を付けるかを乱数で決めます. (* )
論理式を "$P$" や "$Q$" といった単項式にするか, "($x$ > $y$)" にするかを乱数で決めます.
1. 単項式が選ばれた場合はそれを出力します. 出力時に (* ) の結果に応じて頭に "-" を付けます.
2. "($x$ > $y$)" 型が選ばれた場合は, $x$, $y$ に入る論理式を (* )に戻って作成します. $x$, $y$ が作り終わったら, "($x$ > $y$)" を出力します. 出力時に (* ) の結果に応じて頭に "-" を付けます.

コードは以下の通りです.

a.pl

my $Then = ">";
my $Parentheses_Left = "(";
my $Parentheses_Right = ")";
my $P = "P";
my $Q = "Q";
my $Not = "-";

sub MakeThen {
    my ($Premise, $Consequence) = @_;
    my $Result = $Parentheses_Left.$Premise.$Then.$Consequence.$Parentheses_Right;
    return $Result;
}

sub Sentence {
    my $rand_not = int (rand 2);
    if($rand_not == 0)
    {
        my $rand_then = int (rand 3);
        if ($rand_then == 0)
        {
            return $Not.$P;
        }
        elsif ($rand_then == 1)
        {
            return $Not.$Q;
        }
        elsif ($rand_then == 2)
        {
            return $Not.MakeThen(Sentence(), Sentence());
        }
    }
    elsif($rand_not == 1)
    {
        my $rand_then = int (rand 3);
        if ($rand_then == 0)
        {
            return $P;
        }
        elsif ($rand_then == 1)
        {
            return $Q;
        }
        elsif ($rand_then == 2)
        {
            return MakeThen(Sentence(), Sentence());
        }
    }
}

トートロジーかどうかの判定

"論理式づくり" の結果, 例えば " (-(-P>-Q)>Q) " のような論理式(文字列)が出力されてきます. これがトートロジーかどうかを判定します. トートロジーとは, 命題の真偽に関わらず真の値を返す論理式のことですので, "P" や "Q" に真偽を代入して" (-(-P>-Q)>Q) "の値を確認 すればよさそうです. 太字部分は以下のように行えます. 以下, 真(True), 偽(False) をそれぞれ T, F であらわします.

($P$, $Q$) = ($\textrm{True}$, $\textrm{True}$) を代入してチェックする.
1. 文字列 "(-(-P>-Q)>Q)" の "P" を "T", "Q" を "T" でそれぞれ置き換える.
  結果, "(-(-T>-T)>T)" になります.
2. 以下のように文字列の置換を行います. 例えば, "(-(-T>-T)>T)" は一回目では "(-(F>F)>T)" に置換されます.
  - "-F", "(T>T)", "(F>T)", "(F>F)" は "T" で置換.
  - "-T", "(T>F)" は "F" で置換.
3. "T" か "F" の一文字になるまで 2. を繰り返す. "(-(F>F)>T)" が "(-T>T)", "(F>T)", "T" と置換されていきます. 残った文字が, この場合の論理式の値になっています.
($P$, $Q$) = ($\textrm{True}$, $\textrm{True}$)以外を代入して同様にチェックする.
すべての場合に "T" になれば元の論理式はトートロジーです.

置換部分のコードは例えば

a.pl

sub Judge {
    my ($Candidate) = @_;
    while (length($Candidate) > 1)
    {
        #Not
        $Candidate =~ s/(?:-T)/F/g;
        $Candidate =~ s/(?:-F)/T/g;
        #Then
        $Candidate =~ s/(?:\(T>T\))/T/g;
        $Candidate =~ s/(?:\(T>F\))/F/g;
        $Candidate =~ s/(?:\(F>T\))/T/g;
        $Candidate =~ s/(?:\(F>F\))/T/g;
        #print $Candidate."\n";
    }    
    return $Candidate;
}

のような感じです.

論理式の出力(完成)

コンソールに文字列を print するだけです. 同じトートロジーを二度出力しないようにすると, コード全体は以下のようになります.

a.pl

use strict;
use warnings;
use utf8;

binmode STDIN, ':encoding(cp932)';
binmode STDOUT, ':encoding(cp932)';
binmode STDERR, ':encoding(cp932)';

my $Then = ">";
my $Parentheses_Left = "(";
my $Parentheses_Right = ")";
my $P = "P";
my $Q = "Q";
my $Not = "-";

my @Memory;
my $number = 0;
my $loop = 0;
my $already = 0;

sub MakeThen {
    my ($Premise, $Consequence) = @_;
    my $Result = $Parentheses_Left.$Premise.$Then.$Consequence.$Parentheses_Right;
    return $Result;
}

sub Sentence {
    my $rand_not = int (rand 2);
    if($rand_not == 0)
    {
        my $rand_then = int (rand 3);
        if ($rand_then == 0)
        {
            return $Not.$P;
        }
        elsif ($rand_then == 1)
        {
            return $Not.$Q;
        }
        elsif ($rand_then == 2)
        {
            return $Not.MakeThen(Sentence(), Sentence());
        }
    }
    elsif($rand_not == 1)
    {
        my $rand_then = int (rand 3);
        if ($rand_then == 0)
        {
            return $P;
        }
        elsif ($rand_then == 1)
        {
            return $Q;
        }
        elsif ($rand_then == 2)
        {
            return MakeThen(Sentence(), Sentence());
        }
    }
}

sub Judge {
    my ($Candidate) = @_;
    while (length($Candidate) > 1)
    {
        #Not
        $Candidate =~ s/(?:-T)/F/g;
        $Candidate =~ s/(?:-F)/T/g;
        #Then
        $Candidate =~ s/(?:\(T>T\))/T/g;
        $Candidate =~ s/(?:\(T>F\))/F/g;
        $Candidate =~ s/(?:\(F>T\))/T/g;
        $Candidate =~ s/(?:\(F>F\))/T/g;
        #print $Candidate."\n";
    }    
    return $Candidate;
}

while(1)
{
    my $Proposition = Sentence();
    #print $Proposition."\n";

    # Judgement
    my $Original = $Proposition;

    # (P,Q) = (T,T) 
    $Proposition = $Original;
    $Proposition =~ s/[P]/T/g;
    $Proposition =~ s/[Q]/T/g;
    #print Judge($Proposition)." when P is True and Q is True\n";
    if(Judge($Proposition) eq "F")
    {
        next;
    }
    # (P,Q) = (T,F) 
    $Proposition = $Original;
    $Proposition =~ s/[P]/T/g;
    $Proposition =~ s/[Q]/F/g;
    #print Judge($Proposition)." when P is True and Q is False\n";
    if(Judge($Proposition) eq "F")
    {
        next;
    }
    # (P,Q) = (F,T) 
    $Proposition = $Original;
    $Proposition =~ s/[P]/F/g;
    $Proposition =~ s/[Q]/T/g;
    #print Judge($Proposition)." when P is False and Q is True\n";
    if(Judge($Proposition) eq "F")
    {
        next;
    }
    # (P,Q) = (F,F) 
    $Proposition = $Original;
    $Proposition =~ s/[P]/F/g;
    $Proposition =~ s/[Q]/F/g;
    #print Judge($Proposition)." when P is False and Q is False\n";
    if(Judge($Proposition) eq "F")
    {
        next;
    }
    
    $already = 0;
    for($loop = 0; $loop < $number; $loop++)
    {
        if($Memory[$loop] eq $Original)
        {
            $already = 1;
        }
    }
    if($already == 1)
    {
        next;
    }
    $Memory[$number] = $Original;
    $number ++;
    print $Original."\n";
}

これを実行すると, (コンソール上に ?) 様々なトートロジーが流れてきます. はじめは, "(P>P)" といった自明なものや "(P>(Q>-(Q>-P)))" のような面白いものが出力され, 時間が経つと, "(-(-(P>(Q>-(P>(Q>-(-(-(-P>-(P>Q))>-P)>(-P>-(-Q>P)))))))>Q)>-Q)"のような難しい式が出てきて楽しいです.