等式論理

equational-theorem.kt

interface Substitution {
    fun with(vararg ps: Predicate): Predicate
}

interface Predicate {
    fun substitute(vararg xs: Symbol): Substitution
}

data class Symbol(val name: String) : Predicate {
    override fun toString(): String = name

    override fun substitute(vararg xs: Symbol): Substitution =
        object: Substitution {
            override fun with(vararg ps: Predicate): Predicate =
                xs.zip(ps).find { (x, _) -> x.name == name }?.second ?: this@Symbol
        }
}

data class Equation(val left: Predicate, val right: Predicate) : Predicate {
    override fun toString(): String = "($left = $right)"

    override fun substitute(vararg xs: Symbol): Substitution =
        object: Substitution {
            override fun with(vararg ps: Predicate): Predicate =
                Equation(left.substitute(*xs).with(*ps), right.substitute(*xs).with(*ps))
        }
}

infix fun Equation.leibniz(e: Substitution): Equation =
    Equation(e.with(left), e.with(right))

infix fun Equation.transitivity(e: Equation): Equation =
    if (right == e.left) {
        Equation(left, e.right)
    } else {
        throw IllegalArgumentException("The right hand side of $this does not match the left hand side of $e.")
    }

infix fun Predicate.equanimity(e: Equation): Predicate =
    if (this == e.left) {
        e.right
    } else {
        throw IllegalArgumentException("$this does not match the left hand side of equation $e.")
    }

Leibniz 則は Equation に生やした leibniz によって起動する。

// P=Q / (p=x)[x:= P] = (p=x)[x:= Q] ; => (p = P) = (p = Q)
Equation(Symbol("P"), Symbol("Q"))
  .leibniz(Equation(Symbol("p"),Symbol("x")).substitute(Symbol("x")))

Transitivity:

// P=Q Q=R / P=R
Equation(Symbol("P"), Symbol("Q"))
  .transitivity(Equation(Symbol("Q"), Symbol("R")))

および Equanimity:

// P P=Q / Q
Symbol("P")
  .equanimity(Equation(Symbol("P"), Symbol("Q")))