小野寛晰『情報科学における論理』の読書ノート。（→前回）
第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
まずは論理式、式、証明図といったモデルたち。
interface Formula {
readonly identifier?: string;
readonly operator?: Operator;
readonly operand1?: Formula;
readonly operand2?: Formula;
}
type Formulas = ReadonlyArray<Formula>;
interface Sequent {
readonly antecedents: Formulas;
readonly succedents: Formulas;
}
interface ProofTree {
readonly height: number;
readonly root: ProofTreeNode;
}
interface ProofTreeNode {
readonly level: number;
readonly sequent: Sequent;
readonly left?: ProofTreeNode;
readonly right?: ProofTreeNode;
}
そして推論規則。式（＝上式）を引数に長さ1または2の式のタプル（＝下式）を返す関数として表現した。ここでは∧Lと∧Rを抜萃。
type InferenceRule = (sequent: Sequent, position: number) => [Sequent, Sequent?];
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)];
};
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])
];
};
推論規則を使って論理結合子がなくなるまで式の分解を繰り返す完全分解木（証明図）生成ゾーン。完全分解木の葉がすべて始式であれば与えられた式は証明可能、すなわちトートロジーであると判断する。
@paramthe
@return
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;
}
}
return false;
};
@paramsequent
@return
const decompose: (sequent: Sequent) => [Sequent, Sequent?] | null = (sequent: Sequent) => {
let position = sequent.antecedents.findIndex(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);
};
@paramsequent
@return
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 };
}
};
動かすとこんな感じ。例はド・モルガンの定理。
（→次回）
