ノート: 情報科学における論理②

小野寛晰『情報科学における論理』の読書ノート。（→前回）

第1章 命題論理（承前）

今回はシークエント計算を実装してみる。

定理1.8の証明で登場した式の分解を推論規則に、完全分解木を証明図に流用したいので、形式体系LKそのままではなくそれを少し変形した形式体系LK'を新たに定義して実装する。

形式体系LK'

用意した推論規則は次の8つ。ラテン文字は論理式、ギリシア文字は長さ0以上の論理式の列とする。

∧ Left (∧L)

∧ Right (∧R)

∨ Left (∨L)

∨ Right (∨R)

→ Left (→L)

→ Right (→R)

¬ Left (¬L)

¬ Right (¬R)

始式には を採用する。

実装

TypeScriptで実装。ソース全体は↓。

github.com

まずは論理式、式、証明図といったモデルたち。

/**
 * Represents a logical formula.
 */
interface Formula {
    /** Gets the identifier if this formula is a propositional variable, `undefined` otherwise. */
    readonly identifier?: string;

    /** Gets the operator if this formula is a compound formula, `undefined` otherwise. */
    readonly operator?: Operator;

    /** Gets the first operand if this formula is a compound formula, `undefined` otherwise. */
    readonly operand1?: Formula;

    /** Gets the second operand if this formula is a compound formula and the operator is binary, `undefined` otherwise. */
    readonly operand2?: Formula;
}

/**
 * Represents a sequence of zero or more formulas.
 */
type Formulas = ReadonlyArray<Formula>;

/**
 * Represents a sequent.
 */
interface Sequent {
    /** Gets the formula sequence for antecedents. */
    readonly antecedents: Formulas;

    /** Gets the formula sequence for succedents. */
    readonly succedents: Formulas;
}

/**
 * Represents a proof figure as tree structure.
 */
interface ProofTree {
    /** Gets the height of this tree. */
    readonly height: number;

    /** Gets the root node of this tree. */
    readonly root: ProofTreeNode;
}

/**
 * Represents a node of `ProofTree`.
 */
interface ProofTreeNode {
    /** Gets the level of this node. */
    readonly level: number;

    /** Gets the sequent. */
    readonly sequent: Sequent;

    /** Gets the reference to left child node. */
    readonly left?: ProofTreeNode;

    /** Gets the reference to right child node. */
    readonly right?: ProofTreeNode;
}

そして推論規則。式（＝上式）を引数に長さ1または2の式のタプル（＝下式）を返す関数として表現した。ここでは∧Lと∧Rを抜萃。

/**
 * Represents a inference rule.
 */
type InferenceRule = (sequent: Sequent, position: number) => [Sequent, Sequent?];

/**
 * The inference rule that means `&&L`.
 */
const andL: InferenceRule = (s: Sequent, position: number) => {
    const principal = s.antecedents[position];
    const left = s.antecedents.slice(0, position);
    const right = s.antecedents.slice(position + 1);
    return [sequent([...left, principal.operand1!, principal.operand2!, ...right], s.succedents)];
};

/**
 * The inference rule that means `&&R`.
 */
const andR: InferenceRule = (s: Sequent, position: number) => {
    const principal = s.succedents[position];
    const left = s.succedents.slice(0, position);
    const right = s.succedents.slice(position + 1);
    return [
        sequent(s.antecedents, [...left, principal.operand1!, ...right]),
        sequent(s.antecedents, [...left, principal.operand2!, ...right])
    ];
};

推論規則を使って論理結合子がなくなるまで式の分解を繰り返す完全分解木（証明図）生成ゾーン。完全分解木の葉がすべて始式であれば与えられた式は証明可能、すなわちトートロジーであると判断する。

/**
 * Checks whether the specified sequent is an initial sequent.
 *
 * @param the sequent to check
 * @return `true` if the specified sequent is an initial sequent, `false` otherwise
 */
const isInitial: (sequence: Sequent) => boolean = (sequent: Sequent) => {
    for (const i of sequent.antecedents) {
        for (const j of sequent.succedents) {
            if (formequ(i, j)) return true; // formequは論理式の同値関係
        }
    }
    return false;
};

/**
 * Decomposes the specified sequent into one or two sequents.
 *
 * @param sequent the sequent to decompose
 * @return one or two decomposed sequents if possible, `null` otherwise
 */
const decompose: (sequent: Sequent) => [Sequent, Sequent?] | null = (sequent: Sequent) => {
    let position = sequent.antecedents.findIndex(isCompound); // isCompoundは論理式が論理結合子を含んでいるかの述語
    let rule: InferenceRule;
    if (position === -1) {
        position = sequent.succedents.findIndex(isCompound);
        if (position === -1) return null;
        rule = rightRule(sequent.succedents[position].operator!);
    } else {
        rule = leftRule(sequent.antecedents[position].operator!);
    }
    return rule(sequent, position);
};

/**
 * Proves the specified sequent.
 *
 * @param sequent the sequent to prove
 * @return the proof result
 */
const prove: (sequent: Sequent) => Proof = (sequent: Sequent) => {
    let provable = true;
    let maxLv = 0;
    const makeTree: (s: Sequent, level: number) => ProofTreeNode = (s: Sequent, level: number) => {
        if (!provable) return { level, sequent: s };
        const decomposed = decompose(s);
        if (!decomposed) {
            provable = provable && isInitial(s);
            maxLv = Math.max(maxLv, level);
            return { level, sequent: s };
        }
        if (decomposed[1]) {
            return {
                level,
                sequent: s,
                left: makeTree(decomposed[0], level + 1),
                right: makeTree(decomposed[1], level + 1)
            };
        } else {
            return {
                level,
                sequent: s,
                left: makeTree(decomposed[0], level + 1)
            };
        }
    };
    const root = makeTree(sequent, 0);
    if (provable) {
        return {
            provable,
            figure: {
                height: maxLv + 1,
                root
            }
        };
    } else {
        return { provable };
    }
};

動かすとこんな感じ。例はド・モルガンの定理。

（→次回）