2
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

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

Posted at

はじめに

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

参考になった記事

そもそも 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$" と書きます. 論理式は以下のように再帰的に定義された関数から出力されます.

  1. 論理式の頭に "-" ("not") を付けるかを乱数で決めます. (* )
  2. 論理式を "$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 であらわします.

  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" になれば元の論理式はトートロジーです.

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

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

2
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
2
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?