MathStuff/logic.rb at master · jedediah/MathStuff · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
require_relative 'ext'
require_relative 'expr'
require_relative 'set'

module Logic
    class << self
        def quantify(op, &block)
            formula, *vars = Variable.call_with_vars(&block)
            vars.reverse_each do |var|
                formula = op.new(var, formula)
            end
            formula
        end

        def any?(&block)
            quantify(ThereExists, &block)
        end

        def all?(&block)
            quantify(ForAll, &block)
        end
    end

    module Formula
        include Expr

        class << self
            def coerce(*xs)
                xs.map do |x|
                    if x.is_a? Formula
                        x
                    else
                        raise TypeError, "#{x} is not a logical formula"
                    end
                end
            end
        end

        def ~
            Not.new(self)
        end

        def &(x)
            And.new(self, x)
        end

        def |(x)
            Or.new(self, x)
        end

        def ^(x)
            Xor.new(self, x)
        end

        def >>(x)
            Implies.new(self, x)
        end

        def <<(x)
            Implies.new(x, self)
        end

        def ==(x)
            Equivalent.new(self, x)
        end
    end

    module Predicate
        include Formula
        # include Operation
        #
        # attr :name, :args
        #
        # def initialize(name, *args)
        #     @name = name.to_sym
        #     @args = args.freeze
        # end
        #
        # def eql?(x)
        #     x.is_a?(Predicate) && name == x.name && args == x.args
        # end
    end

    class Quantifier
        include Operation
        include Formula

        attr :variable

        def initialize(variable, arg)
            @variable = variable
            super(arg)
        end

        def inspect
            "#{name} #{variable.inspect} | #{args[0].inspect}"
        end

        def inspect_latex
            "#{name_latex} #{variable.inspect_latex} \\mid #{args[0].inspect_latex}"
        end

        def eql?(x)
            x.is_a?(Quantifier) && name == x.name && variable == x.variable && args[0] == x.args[0]
        end

        def free_variables
            args[0].free_variables.without(variable)
        end
    end

    class ThereExists < Quantifier
        attr_const name: '∃',
                   name_latex: '\\exists'
    end

    class ForAll < Quantifier
        attr_const name: '∀',
                   name_latex: '\\forall'
    end

    class Not
        include PrefixOp
        include Formula

        attr_const name: '¬',
                   name_latex: '\\neg'

        handleop :~, Formula
    end

    class And
        include InfixOp
        include Formula

        attr_const name: '∧',
                   name_latex: '\\wedge'

        handleop :&, Formula, Formula
    end

    class Or
        include InfixOp
        include Formula
        attr_const name: '∨',
                   name_latex: '\\vee'
    end

    class Xor
        include InfixOp
        include Formula
        attr_const name: '⊕',
                   name_latex: '\\oplus'
    end

    class Implies
        include InfixOp
        include Formula
        attr_const name: '⇒',
                   name_latex: '\\Rightarrow'
    end

    class Equivalent
        include InfixOp
        include Formula
        attr_const name: '⇔',
                   name_latex: '\\Leftrightarrow'
    end
end