はじめに
むかしむかしに スマリヤンの本 を読んで以来, 作りたいと思っていた表題のプログラムを実装した記録です.
参考になった記事
そもそも 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$)" にするかを乱数で決めます.
- 単項式が選ばれた場合はそれを出力します. 出力時に (* ) の結果に応じて頭に "-" を付けます.
- "($x$ > $y$)" 型が選ばれた場合は, $x$, $y$ に入る論理式を (* )に戻って作成します. $x$, $y$ が作り終わったら, "($x$ > $y$)" を出力します. 出力時に (* ) の結果に応じて頭に "-" を付けます.
コードは以下の通りです.
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}$) を代入してチェックする.
- 文字列 "(-(-P>-Q)>Q)" の "P" を "T", "Q" を "T" でそれぞれ置き換える.
結果, "(-(-T>-T)>T)" になります. - 以下のように文字列の置換を行います. 例えば, "(-(-T>-T)>T)" は一回目では "(-(F>F)>T)" に置換されます.
- "-F", "(T>T)", "(F>T)", "(F>F)" は "T" で置換.
- "-T", "(T>F)" は "F" で置換.
- "T" か "F" の一文字になるまで 2. を繰り返す. "(-(F>F)>T)" が "(-T>T)", "(F>T)", "T" と置換されていきます. 残った文字が, この場合の論理式の値になっています.
- 文字列 "(-(-P>-Q)>Q)" の "P" を "T", "Q" を "T" でそれぞれ置き換える.
-
($P$, $Q$) = ($\textrm{True}$, $\textrm{True}$)以外 を代入して同様にチェックする.
-
すべての場合に "T" になれば元の論理式はトートロジーです.
置換部分のコードは例えば
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 するだけです. 同じトートロジーを二度出力しないようにすると, コード全体は以下のようになります.
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)"のような難しい式が出てきて楽しいです.