#!/usr/bin/perl
#
# $Id: mally.pl,v 1.19 2002/07/02 10:24:48 lokhorst Exp $
#
# Supplement to G.J.C. Lokhorst, "Mally's Deontic Logic",
# in Edward N. Zalta, ed., Stanford Encyclopedia of Philosophy.
# The Metaphysics Research Lab at the Center for the Study of
# Language and Information, Stanford University, Stanford, CA,
# 2002.
#
# Perl script that can also be run as a cgi program.
#

use strict;

$count::main = 0;

sub definitionA {

    # These matrices were discovered by MaGIC version 2.1.4:
    # see the output of MaGIC at the end of this program.
    @values::main    = ( 0 .. 5 );
    @matrixNeg::main = reverse @values::main;
    @matrixCon::main = (
        [ 0, 0, 0, 0, 0, 0 ], [ 0, 1, 0, 1, 0, 1 ],
        [ 0, 0, 2, 2, 2, 2 ], [ 0, 1, 2, 3, 2, 3 ],
        [ 0, 0, 2, 2, 4, 4 ], [ 0, 1, 2, 3, 4, 5 ],
    );
    @matrixArrow::main = (
        [ 5, 5, 5, 5, 5, 5 ], [ 0, 1, 2, 3, 4, 5 ],
        [ 0, 0, 1, 1, 3, 5 ], [ 0, 0, 0, 1, 2, 5 ],
        [ 0, 0, 0, 0, 1, 5 ], [ 0, 0, 0, 0, 0, 5 ],
    );
    @matrixObl::main = ( 0, 0, 1, 1, 3, 5 );
    @matrixDes::main = ( 0, 1, 0, 1, 0, 1 );
}

sub definitionB {
    @values::main      = ( 0 .. 2 );
    @matrixNeg::main   = reverse @values::main;
    @matrixCon::main   = ( [ 0, 0, 0 ], [ 0, 1, 1 ], [ 0, 1, 2 ] );
    @matrixArrow::main = ( [ 2, 2, 2 ], [ 0, 1, 2 ], [ 0, 0, 2 ] );
    @matrixObl::main   = @values::main;
    @matrixDes::main = ( 0, 1, 1 );
}

# connectives
# Internal notation: fully parenthesized prefix notation
$V::main = 1;
$U::main = 2;

# conjunction
sub K {
    return @matrixCon::main[ $_[0] ]->[ $_[1] ];
}

# relevant implication
sub C {
    return @matrixArrow::main[ $_[0] ]->[ $_[1] ];
}

# negation
sub N {
    return @matrixNeg::main[ $_[0] ];
}

# obligation
sub O {
    return @matrixObl::main[ $_[0] ];
}

# disjunction
sub A {
    return N( K( N( $_[0] ), N( $_[1] ) ) );
}

# equivalence
sub E {
    return K( C( $_[0], $_[1] ), C( $_[1], $_[0] ) );
}

# requirement
sub R {
    return C( $_[0], O( $_[1] ) );
}

# mutual requirement
sub M {
    return K( R( $_[0], $_[1] ), R( $_[1], $_[0] ) );
}

# subroutines for display

# conjunction
sub K_p {
    return "($_[0]" . "&" . "$_[1])";
}

# relevant implication
sub C_p {
    return "($_[0]" . "->" . "$_[1])";
}

# negation
sub N_p {
    return "~" . "$_[0]";
}

# obligation
sub O_p {
    return "!" . "$_[0]";
}

# disjunction
sub A_p {
    return "($_[0]" . "v" . "$_[1])";
}

# equivalence
sub E_p {
    return "($_[0]" . "<->" . "$_[1])";
}

# requirement
sub R_p {
    return "($_[0]" . "f" . "$_[1])";
}

# mutual requirement
sub M_p {
    return "($_[0]" . "<=>" . "$_[1])";
}

sub commify {
    ( @_ == 0 ) ? ".\n" :
      ( @_ == 1 ) ? "$_[0].\n" :
      ( @_ == 2 ) ? join ( " and ", @_ ) . ".\n" :
      join ( ", ", @_[ 0 .. ( $#_ - 1 ) ], "and $_[-1].\n" );
}

sub hdr {
    my ( $name, $conn, $sep ) = @_;
    printf "%s:\n%${sep}s%${sep}s", $name, $conn, "|";

    foreach (@values::main) { printf "%${sep}d", $_ }
    print "\n";
    printf "-" x ( ( 2 * $sep ) - 1 );
    print "+";
    printf "-" x ( scalar(@values::main) * $sep );
    print "\n";
}

sub conn1 {
    my ( $name, $conn, $symbol, $sep ) = @_;
    hdr $name, "", $sep;
    printf "%${sep}s%${sep}s", $symbol, "|";
    foreach my $x (@values::main) { printf "%${sep}d", eval("$conn($x)") }
    print "\n";
}

sub conn2 {
    my ( $name, $conn, $symbol, $sep ) = @_;
    hdr $name, $symbol, $sep;
    foreach my $y (@values::main) {
        printf "%${sep}d%${sep}s", $y, "|";
        foreach my $x (@values::main) {
            printf "%${sep}d", eval("$conn( $y, $x )");
        }
        print "\n";
    }
}

sub showmatrices {
    my @des;
    my $sep = 3;
    print "Admissible values: " . commify(@values::main);
    foreach (@values::main) {
        if ( $matrixDes::main[$_] ) { push ( @des, $_ ) }
    }
    print "Designated values: " . commify(@des);
    printf "Constants: v(V)=%d and v(U)=%d.\n", $V::main, $U::main;
    conn1 'Negation', 'N', '~', $sep;
    conn2 'Relevant Implication', 'C', '->', $sep;
    conn2 'Conjunction', 'K', '&', $sep;
    conn1 'Obligation',  'O', '!', $sep;
    conn2 'Disjunction', 'A', 'v', $sep;
    conn2 'Relevant Equivalence', 'E', '<->', $sep;
    conn2 'Requirement',        'R', 'f',   $sep;
    conn2 'Mutual Requirement', 'M', '<=>', $sep;
}

sub showformula {
    my ( $name, $wff, $result ) = @_;
    printf "%-12s%-32s%s", $name, $wff, $result;
}

# subroutines for checking
# print and store
sub process {
    my $s;
    my @list;
    my ( $name, $wff, $result ) = @_;

    if ( @$result == 0 ) {
        showformula( $name, $wff, "valid\n" );
        push ( @validnrs::main, $name );
    }
    else {

        $s = "v($name)=@$result[0]";
        if ( @$result > 1 ) {
            $s = $s . " if ";
            push ( @list, "v(A)=@$result[1]" );
            if ( @$result > 2 ) {
                push ( @list, "v(B)=@$result[2]" );

                if ( @$result > 3 ) {
                    push ( @list, "v(C)=@$result[3]" );

                    if ( @$result > 4 ) {
                        push ( @list, "v(D)=@$result[4]" );
                    }
                }
            }
        }
        showformula( $name, $wff, $s . commify(@list) );
        push ( @invalidnrs::main, $name );
    }
}

# returns string in infix notation
sub wffstr {
    my ($wff) = @_;
    $wff =~ s/([A-Z])/${1}_p/g;
    my ( $a, $b, $c, $d, $u, $v ) = ( "A", "B", "C", "D", "U", "V" );
    return eval($wff);
}

# main loops
sub check {
    my $u = $U::main;
    my $v = $V::main;
    my ( $name, $wff ) = @_;
    my @msg;

    if ( $wff =~ /\$d/ ) {
        CHECK4:
        foreach my $a (@values::main) {
            foreach my $b (@values::main) {
                foreach my $c (@values::main) {

                    foreach my $d (@values::main) {
                        my $z = eval($wff);
                        $count::main++;
                        if ( !$matrixDes::main[$z] ) {
                            @msg = ( $z, $a, $b, $c, $d );
                            last CHECK4;
                        }
                    }
                }
            }
        }
    }
    elsif ( $wff =~ /\$c/ ) {
        CHECK3:

        foreach my $a (@values::main) {
            foreach my $b (@values::main) {
                foreach my $c (@values::main) {
                    my $z = eval($wff);
                    $count::main++;

                    if ( !$matrixDes::main[$z] ) {
                        @msg = ( $z, $a, $b, $c );
                        last CHECK3;
                    }
                }
            }
        }
    }

    elsif ( $wff =~ /\$b/ ) {
        CHECK2:
        foreach my $a (@values::main) {
            foreach my $b (@values::main) {
                my $z = eval($wff);
                $count::main++;

                if ( !$matrixDes::main[$z] ) {
                    @msg = ( $z, $a, $b );
                    last CHECK2;
                }
            }
        }
    }
    elsif ( $wff =~ /\$a/ ) {
        CHECK1:

        foreach my $a (@values::main) {
            my $z = eval($wff);
            $count::main++;

            if ( !$matrixDes::main[$z] ) {
                @msg = ( $z, $a );
                last CHECK1;
            }
        }
    }
    else {
        my $z = eval($wff);
        $count::main++;

        if ( !$matrixDes::main[$z] ) {
            @msg = ($z);
        }
    }

    process( $name, wffstr($wff), \@msg );
}

sub checkrule {
    my $u = $U::main;
    my $v = $V::main;
    my ( $name, $wff0, $wff1, $wff2 ) = @_;
    my @msg;
    CheckRule2:

    foreach my $a (@values::main) {
        if ( $matrixDes::main[ eval($wff0) ] ) {
            foreach my $b (@values::main) {
                if ( $matrixDes::main[ eval($wff1) ] ) {
                    my $z = eval($wff2);
                    $count::main++;

                    if ( !$matrixDes::main[$z] ) {
                        @msg = ( $z, $a, $b );
                        last CheckRule2;
                    }
                }
            }
        }
    }

    my $s = wffstr($wff0) . "," . wffstr($wff1) . "/" . wffstr($wff2);
    process( $name, $s, \@msg );
}

# tests
sub testformulas {
    my $prime = "'";
    @validnrs::main   = ();
    @invalidnrs::main = ();

    printf "## %d-valued matrices\n", scalar(@values::main);
    showmatrices;

    print "## Alethic Axioms\n";

    check( "Self-impl",  'C($a,$a)' );
    check( "Pref",       'C(C($a,$b),C(C($c,$a),C($c,$b)))' );
    check( "Contract",   'C(C($a,C($a,$b)),C($a,$b))' );
    check( "Perm",       'C(C($a,C($b,$c)),C($b,C($a,$c)))' );
    check( "A<->(V->A)", 'E($a,C($v,$a))' );
    check( "DblNeg",     'C(N(N($a)),$a)' );
    check( "Contrapos",  'C(C($a,N($b)),C($b,N($a)))' );
    check( "&-Elim1",    'C(K($a,$b),$a)' );
    check( "&-Elim2",    'C(K($a,$b),$b)' );
    check( "&-Int",      'C(K(C($a,$b),C($a,$c)),C($a,K($b,$c)))' );
    check( "v-Int1",     'C($a,A($a,$b))' );
    check( "v-Int2",     'C($b,A($a,$b))' );
    check( "v-Elim",     'C(K(C($a,$c),C($b,$c)),C(A($a,$b),$c))' );
    check( "Distr",      'C(K($a,(A($b,$c))),A(K($a,$b),$c))' );

    print "## Rules of Inference\n";

    checkrule( "MP",  '$a', 'C($a,$b)', '$b' );
    checkrule( "Adj", '$a', '$b',       'K($a,$b)' );

    print "## Deontic Axioms\n";

    check( "I",   'C(K(R($a,$b),C($b,$c)),R($a,$c))' );
    check( "II",  'C(K(R($a,$b),R($a,$c)),R($a,K($b,$c)))' );
    check( "III", 'E(R($a,$b),O(C($a,$b)))' );
    check( "IV",  'O($u)' );
    check( "V",   'N(R($u,N($u)))' );

    print "## Formulas (Mally/Menger/Anderson)\n";

    check( "01",       'C(R($a,$b),R($a,$v))' );
    check( "02",       'C(R($a,N($v)),R($a,$b))' );
    check( "03",       'C(A(R($a,$b),R($a,$c)),R($a,A($b,$c)))' );
    check( "04",       'C(K(R($a,$b),R($c,$d)),R(K($a,$c),K($b,$d)))' );
    check( "05",       'K(C(O($a),R($b,$a)),C(R($v,$a),O($a)))' );
    check( "06",       'R(K(O($a),C($a,$b)),$b)' );
    check( "07",       'C(O($a),O($v))' );
    check( "08",       'C(K(R($a,$b),R($b,$c)),R($a,$c))' );
    check( "09",       'R(K(O($a),R($a,$b)),$b)' );
    check( "10",       'E(K(O($a),O($b)),O(K($a,$b)))' );
    check( "11",       'E(M($a,$b),O(E($a,$b)))' );
    check( "12",       'E(O(C($a,$b)),O(N(K($a,N($b)))))' );
    check( "13",       'E(R($a,$b),N(K($a,N(O($b)))))' );
    check( "14",       'E(R($a,$b),R(N($b),N($a)))' );
    check( "15",       'R($a,$u)' );
    check( "16",       'R(C($u,$a),$a)' );
    check( "17",       'R(R($u,$a),$a)' );
    check( "18",       'C(O(O($a)),O($a))' );
    check( "19",       'E(O(O($a)),O($a))' );
    check( "20",       'E(R($u,$a),M($a,$u))' );
    check( "21",       'E(O($a),M($a,$u))' );
    check( "22",       'O($v)' );
    check( "23",       'M($v,$u)' );
    check( "23$prime", 'R($v,$u)' );
    check( "24",       'R($a,$a)' );
    check( "25",       'C(C($a,$b),R($a,$b))' );
    check( "26",       'C(E($a,$b),M($a,$b))' );
    check( "27",       'R(N($u),$a)' );
    check( "28",       'R(N($u),N($u))' );
    check( "29",       'R(N($u),$u)' );
    check( "30",       'R(N($u),N($v))' );
    check( "31",       'M(N($u),N($v))' );
    check( "32",       'N(R($u,N($v)))' );
    check( "33",       'N(C($u,N($v)))' );
    check( "34",       'E($u,$v)' );
    check( "35",       'E(N($u),N($v))' );
    check( "A<->!A",   'E($a,O($a))' );
    check( "ARD1->",   'C(O($a),C(N($a),N($u)))' );
    check( "ARD1<-",   'C(C(N($a),N($u)),O($a))' );
    check( "ARD2",     'C(O($a),N(O(N($a))))' );

    printf "## Summary (%d-valued matrices)\n", scalar(@values::main);
    print "Valid formulas: " . commify(@validnrs::main);
    print "Invalid formulas: " . commify(@invalidnrs::main);
    if ( scalar(@values::main) == 6 ) { @invalidnrs6::main = @invalidnrs::main }
    elsif ( scalar(@values::main) == 3 ) {
        @invalidnrs3::main = @invalidnrs::main;
    }
}

sub summary {
    print "## Global summary\n";
    print "Formulas that are invalid according to either ";
    print "the 3-valued or the 6-valued matrices: ";
    my %union;

    foreach my $e (@invalidnrs6::main) { $union{$e} = 1 }
    foreach my $e (@invalidnrs3::main) { $union{$e} = 1 }
    print commify( sort { $a cmp $b } keys %union );
    printf "## Done. %d values tested.\n", $count::main;
}

# Main program
# next line turns this program into a cgi program
print "Content-type: text/plain\n\n";

definitionA;
testformulas;
definitionB;
testformulas;
summary;
exit;

# Output from MaGIC. Definition: u o u = ~(u -> ~u).
#
# Logic: R
# Extra: (u o u) o u
# Fragment: ->, &, v, ~, o, t, f, T, F
# Definition: u Primitive (cut)
# Fail: u o u
# Search concludes when 1 matrix found
# or when size 14 finished.
#
# Size: 6
#
# Negation table 6.1
#  a| 0 1 2 3 4 5
# --+------------
# ~a| 5 4 3 2 1 0
#
# Order 6.1.1
# < | 0 1 2 3 4 5
# --+------------
# 0 | + + + + + +
# 1 | - + - + - +
# 2 | - - + + + +
# 3 | - - - + - +
# 4 | - - - - + +
# 5 | - - - - - +
#
# Choice 6.1.1.1 of t: 1
#
# Implication matrix 6.1.1.1.1
# ->| 0 1 2 3 4 5
# --+------------
# 0 | 5 5 5 5 5 5
# 1 | 0 1 2 3 4 5
# 2 | 0 0 1 1 3 5
# 3 | 0 0 0 1 2 5
# 4 | 0 0 0 0 1 5
# 5 | 0 0 0 0 0 5
# Choice 6.1.1.1.1.1 of u: 2
# Failure: u o u
#
# That's all, for now.