トートロジーをランダムに出力する Perl プログラム 

# はじめに
 むかしむかしに [スマリヤンの本](http://www.hakuyo-sha.co.jp/mathematics/%E3%82%B9%E3%83%9E%E3%83%AA%E3%83%A4%E3%83%B3%E3%81%AE%E6%B1%BA%E5%AE%9A%E4%B8%8D%E8%83%BD%E3%81%AE%E8%AB%96%E7%90%86%E3%83%91%E3%82%BA%E3%83%AB/) を読んで以来, 作りたいと思っていた表題のプログラムを実装した記録です.

# 参考になった記事
そもそも perl を初めて触ったので以下のような記事が参考になりました.
[perl 入門](https://www.javadrive.jp/perl/)
[perl での関数の再帰的定義](http://m-shige1979.hatenablog.com/entry/2014/08/04/080000)
[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 は以下のように定義されます.

```math
\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" の組み合わせで書ける, というのがあります.  
        - 定義は,  
        
```math
\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$" と書きます. 論理式は以下のように再帰的に定義された関数から出力されます. 

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

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

``` perl: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 であらわします. 

1. ($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" と置換されていきます. 残った文字が, この場合の論理式の値になっています.

2. ($P$, $Q$) = ($\textrm{True}$, $\textrm{True}$)以外 を代入して同様にチェックする. 
3. すべての場合に "T" になれば元の論理式はトートロジーです.

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

``` perl: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 するだけです. 同じトートロジーを二度出力しないようにすると, コード全体は以下のようになります.

```perl: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)"のような難しい式が出てきて楽しいです.