等式論理

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.")
    }

等式論理による証明補助の基礎。

述語（Predicate）はその中にあらわれるシンボル（これも述語）を置換（Substitution）でき、置換によって生成された述語は同じ真偽値を持つ。
実装上のポイントは Substitution を生成する substitute 関数の引数が vararg で、同時代入を組み込みでサポートするところ。
実際の置換は Substitution の with 関数によって起動する。こちらも引数は vararg。シンボルを対応する述語で置き換える。

// ((p = q) = r)[p,q:= p = q, p] ; => ((p = q) = q) = p
Equation(Equation(Symbol("p"), Symbol("q")), Symbol("r"))
  .substitute(Symbol("p"), Symbol("q"))
  .with(Equation(Symbol("p"), Symbol("q")), Symbol("p"))

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")))