JavaScript で論理学を実装

0. 概要

JavaScript上で命題論理の言語を実装し、意味論 (恒真式・意味論的同値関係やタブロー計算)の各種概念も実装に落とし込む。証明論は未実装。動作環境は Node。

依存パッケージは nearley (構文解析) のみ。npm i --save nearley で環境構築完了。

0. 表記

原子命題は p,q,r,s,t,u のみ利用可。¬⋀⋁→↔ は -,A,V,->,== とする。よって例えば、$\neg\neg p \leftrightarrow p$ は --p == p となるし、$\neg(p\wedge q)\leftrightarrow \neg p \vee \neg q$ は -(p A q) == -p V -qとなる。

1. 統語論 ～構文木の構築～

文字列を構文木にする。木構造には JavaScript の Array を利用する。具体的には pAq を ['A','p','r'], pVqAr を ['V','p',['A','q','r']] というようにしたい。構文解析器は Nearley を利用して作る。命題論理の文法を以下に記載:

grammar.ns

@builtin "whitespace.ne"

formula -> _ equ _ {% d => d[1] %}
equ -> equ eq imp {% ([a1,op,a2]) => [op, a1, a2] %}
  | imp           {% id %}
imp -> disj then imp {% ([a1,op,a2]) => [op, a1, a2] %}
  | disj             {% id %}
disj -> disj or conj {% ([a1,op,a2]) => [op, a1, a2] %}
  | conj             {% id %}
conj -> conj and lit {% ([a1,op,a2]) => [op, a1, a2] %}
  | lit              {% id %}
lit -> not lit {% ([op,a]) => [op, a] %}
  | prime      {% id %}
prime -> [p-uTF] {% id %}
  | pf         {% id %}
pf -> "(" formula ")" {% d => d[1] %}

# op
not -> "-" _ {% id %}
and -> _ "A" _ {% d => d[1] %}
or -> _ "V"  _ {% d => d[1] %}
then -> _ "->" _  {% d => d[1] %}
eq -> _ "==" _ {% d => d[1] %}

以下のコマンドで文法をコンパイル:

npx nearleyc grammar.ne -o grammar.js

こうして構文木を構築する関数を実装できる:

const nearley = require('nearley');
const grammar = require('./grammar.js');

function syntaxTreeOf (str) {
  const parser = new nearley.Parser(nearley.Grammar.fromCompiled(grammar));
  parser.feed(str);
  if (parser.results.length === 0) {
    throw Error('parser returns no formula.');
  } else if (parser.results.length !== 1) {
    console.log(`Ambiguious: ${parser.results.length}ways`);
    parser.results.forEach(r => console.log(r));
  }
  return parser.results[0];
}

2. 意味論

2.1 意味論的値

論理式に登場する 原子命題 に false もしくは true の値を割り振ると、帰納的に 論理式の値が定まる。

したがって、値の割り当てとは「true に評価される原子命題記号の集合」を指定することであるとみなせるので、そのような シグネチャにする。つまり、入力として 構文木 と true に評価される原子命題記号 が与えられたときに、論理式の意味論的値を出力するコードは以下:

意味論的値を求めるための関数.js

const VAR = ['p', 'q', 'r', 's', 't', 'u'];
function semanticValueOf (tree, primes) {
  // for primes
  const dic = { T: true, F: false };
  VAR.forEach(v => { dic[v] = primes.includes(v); });
  // recursive definition
  const valOf = tree => {
    // prime
    if (typeof tree === 'string') {
      return dic[tree];
    }
    const [op, a1, a2] = tree;
    // compound
    if (op === '-') {
      return !valOf(a1);
    } else if (op === 'A') {
      return valOf(a1) && valOf(a2);
    } else if (op === 'V') {
      return valOf(a1) || valOf(a2);
    } else if (op === '->') {
      return !valOf(a1) || valOf(a2);
    } else if (op === '==') {
      return (valOf(a1) && valOf(a2)) || (!valOf(a1) && !valOf(a2));
    }
    console.log(tree);
    throw Error('cannnot reach here');
  };
  // do it
  return valOf(tree);
}

2.2 トートロジー

任意の割り当てで意味論的値が1な論理式をトートロジーという。論理式がトートロジーであることを確認する関数を作成する。論理式に含まれるn個の変数の一覧を求め、それらへの値の割り当て $2^n$ 通りに対し、意味論的値が 全て 1であることを確認すればよい。

まずは、論理式に登場する 原子命題記号の一覧を取得するための関数 varOf を実装する。えられた n個の命題記号に対する値の割り当てを以下の手順で作る: 割り当てに 0..2^n-1 の識別子 m を与える。m の2進表現の 1bit 目が立っていたら、1個目の原子命題が true な割り当て、2bit目が立っていたら、2個目の原子命題が true な割り当て・・・とする。

よって以下のように実装できる:

トートロジーのチェック.js

function varOf (tree) {
  const recFn = (root) => {
    if (typeof root === 'string') {
      return [root];
    }
    let result = [];
    for (const f of root.slice(1)) {
      result = result.concat(recFn(f));
    }
    return result;
  };
  return [...new Set(recFn(tree))].sort();
}

function isTaut (tree) {
  const vars = varOf(tree);
  const N = vars.length;
  let result = true;
  for (let i = 0; i < (N << 1); i++) {
    const primes = vars.filter((v, idx) => i & (1 << idx));
    if (!semanticValueOf(tree, primes)) {
      result = false;
      break;
    }
  }
  return result;
}

2.3 意味論的同値関係, 妥当な推論

二つの論理式が、任意の値の割り当てでおなじ意味論的値を取るとき、意味論的同値関係が成立するという。それを判定する関数を作成する。これは簡単。

function isEquivalent (root1, root2) {
  const _vars = [...varOf(root1), ...varOf(root2)];
  const vars = [...new Set(_vars)];
  const N = vars.length;
  let result = true;
  for (let i = 0; i < (N << 1); i++) {
    const primes = vars.filter((v, idx) => i & (1 << idx));
    if (semanticValueOf(root1, primes) !== semanticValueOf(root2, primes)) {
      result = false;
      break;
    }
  }
  return result;
}

推論とは 「N個(N>=0)の論理式を前提として 1つの論理式を結論付ける」という営み。これを意味論的に考察すると、「前提のN 個の論理式が全部 true の値を持つときには いつでも結論の論理式が true の値を持っている」という性質が成立していることが妥当な推論の定義となる。実装はこう:

妥当な推論.js

function isValidInference (premises, conclusion) {
  const _vars = [...premises, conclusion].map(varOf).reduce((a, x) => a.concat(x), []);
  const vars = [...new Set(_vars)];
  const N = vars.length;
  let result = true;
  for (let i = 0; i < (N << 1); i++) {
    const primes = vars.filter((v, idx) => i & (1 << idx));
    if (premises.some(f => !semanticValueOf(f, primes))) {
      continue; // premises not satisfied.
    }
    if (!semanticValueOf(conclusion, primes)) {
      result = false;
      break;
    }
  }
  return result;
}

3. 命題論理の各種定理を確かめる

まずは有名なトートロジーに対して確かめてみた:

有名なトートロジー.js

  const tauts = [
    'p->p',
    '(p->q)->(q->r)->p->r',
    '(p->q->r)->(q->p->r)',
    'p->q->p',
    '(p->q->r)->(p->q)->p->r',
    '((p->q)->p)->p',
  ].map(syntaxTreeOf).every(isTaut);
  console.assert(tauts, 'taut: oops');

ドモルガンの法則をはじめとしたいくつかの有名な同値関係を確かめてみた:

有名な同値関係.js

  const equivs = [
    ['-(pAq)', '-pV-q'], // deMorgan
    ['-(pVq)', '-pA-q'],
    ['pA(qVr)', '(pAq)V(pAr)'], // distriburity
    ['pV(qAr)', '(pVq)A(pVr)'],
    ['p-> qAr', '(p->q)A(p->r)'],
    ['p-> qVr', '(p->q)V(p->r)'],
    ['pAq ->r', '(p->r)V(q->r)'],
    ['pVq ->r', '(p->r)A(q->r)'],
    ['pAq ->r', 'p->q->r'], // deduction theorems
  ].map(p => p.map(syntaxTreeOf)).every(([f1, f2]) => isEquivalent(f1, f2));
  console.assert(equivs, 'equivs: oops');

対偶証明・モーダスポネンスなどの妥当な推論を確認:

妥当な推論.js

  const infer = [
    ['-q->-p', 'p->q'], // contraposition
    ['--p', 'p'], // double-negation
    ['q', 'p', 'p-> q'], // modus ponens
    ['pV-(qVr)', '(pV-q)A(pV-r)'], // bekki p49
    ['(pV-q)A(pV-r)', 'pV-(qVr)'], // bekki p49
    ['p->q->s', 'pAq->r', '-s->(t->u)', 'r->-(t->u)'], // bekki p52
    ['p', '-p->q', 'q->-r', 'rVs', '-s'], // bekki p53
  ].map(p => p.map(syntaxTreeOf)).every(([f, ...fs]) => isValidInference(fs, f));
  console.assert(infer, 'infer: oops');

4. タブロー計算

値の割り当てという観点で、論理式に意味を与えると考えなけらばいけない場合の数が爆発する。同等の結果を生むが 別の意味割り当てによる論理式の計算として、タブロー計算がある。タブロー計算では、恒真式の判定・意味論的同値性の判定・妥当な推論 などなどの概念を表現できる。

説明は、、、、省略

5. ソースコード全体

main.js

const nearley = require('nearley');
const grammar = require('./grammar.js');

function syntaxTreeOf (str) {
  const parser = new nearley.Parser(nearley.Grammar.fromCompiled(grammar));
  parser.feed(str);
  if (parser.results.length === 0) {
    throw Error('parser returns no formula.');
  } else if (parser.results.length !== 1) {
    console.log(`Ambiguious: ${parser.results.length}ways`);
    parser.results.forEach(r => console.log(r));
  }
  return parser.results[0];
}

const VAR = ['p', 'q', 'r', 's', 't', 'u'];
function semanticValueOf (tree, primes) {
  // for primes
  const dic = { T: true, F: false };
  VAR.forEach(v => { dic[v] = primes.includes(v); });
  // recursive definition
  const valOf = tree => {
    // prime
    if (typeof tree === 'string') {
      return dic[tree];
    }
    const [op, a1, a2] = tree;
    // compound
    if (op === '-') {
      return !valOf(a1);
    } else if (op === 'A') {
      return valOf(a1) && valOf(a2);
    } else if (op === 'V') {
      return valOf(a1) || valOf(a2);
    } else if (op === '->') {
      return !valOf(a1) || valOf(a2);
    } else if (op === '==') {
      return (valOf(a1) && valOf(a2)) || (!valOf(a1) && !valOf(a2));
    }
    console.log(tree);
    throw Error('cannnot reach here');
  };
  // do it
  return valOf(tree);
}

function varOf (tree) {
  const recFn = (root) => {
    if (typeof root === 'string') {
      return [root];
    }
    let result = [];
    for (const f of root.slice(1)) {
      result = result.concat(recFn(f));
    }
    return result;
  };
  return [...new Set(recFn(tree))].sort();
}

function isTaut (tree) {
  const vars = varOf(tree);
  const N = vars.length;
  let result = true;
  for (let i = 0; i < (N << 1); i++) {
    const primes = vars.filter((v, idx) => i & (1 << idx));
    if (!semanticValueOf(tree, primes)) {
      result = false;
      break;
    }
  }
  return result;
}

function isEquivalent (root1, root2) {
  const _vars = [...varOf(root1), ...varOf(root2)];
  const vars = [...new Set(_vars)];
  const N = vars.length;
  let result = true;
  for (let i = 0; i < (N << 1); i++) {
    const primes = vars.filter((v, idx) => i & (1 << idx));
    if (semanticValueOf(root1, primes) !== semanticValueOf(root2, primes)) {
      result = false;
      break;
    }
  }
  return result;
}

function isValidInference (premises, conclusion) {
  const _vars = [...premises, conclusion].map(varOf).reduce((a, x) => a.concat(x), []);
  const vars = [...new Set(_vars)];
  const N = vars.length;
  let result = true;
  for (let i = 0; i < (N << 1); i++) {
    const primes = vars.filter((v, idx) => i & (1 << idx));
    if (premises.some(f => !semanticValueOf(f, primes))) {
      continue; // premises not satisfied.
    }
    if (!semanticValueOf(conclusion, primes)) {
      result = false;
      break;
    }
  }
  return result;
}

// ----- from now on, toolset for tablau calc

function isLiteral (f) {
  if (typeof f === 'string') {
    return true;
  }
  return f[0] === '-' && (typeof f[1] === 'string');
}

function pick (_ctx) {
  // TODO: could be more sophisticated.
  const ctx = JSON.parse(JSON.stringify(_ctx));
  const idx = ctx.findIndex(x => !isLiteral(x));
  if (idx === -1) {
    return [null, ctx];
  }
  const picked = ctx.splice(idx, 1)[0];
  return [picked, ctx];
}

// function to check p and -p exists.
function _check (fs) {
  const primes = fs.filter(f => typeof f === 'string');
  return primes.some(p =>
    fs.some(f => typeof f !== 'string' && f[0] === '-' && f[1] === p));
}

function tablauCheck (_ctx) {
  const [target, ctx] = pick(_ctx); // NOTE: ctx is deep copied.
  if (!target) {
    return _check(_ctx); // sorry tablau is probably open.
  }

  const [op, a1, a2] = target;
  if (op === 'A') {
    const next = [...ctx, a1, a2];
    return _check(next) || tablauCheck(next);
  } else if (op === 'V') {
    const n1 = [...ctx, a1];
    const n2 = [...ctx, a2];
    return [n1, n2].every(n => _check(n) || tablauCheck(n));
  } else if (op === '->') {
    const n1 = [...ctx, ['-', a1]];
    const n2 = [...ctx, a2];
    return [n1, n2].every(n => _check(n) || tablauCheck(n));
  } else if (op === '==') {
    const n1 = [...ctx, a1, a2];
    const n2 = [...ctx, ['-', a1], ['-', a2]];
    return [n1, n2].every(n => _check(n) || tablauCheck(n));
  }
  // tableau rule for -, a1 is not prime because target is not literal.
  if (op !== '-') throw Error('something wrong', target);
  if (a1[0] === '-') {
    const n1 = [...ctx, a1[1]];
    return [n1].every(n => _check(n) || tablauCheck(n));
  } else if (a1[0] === 'A') {
    const n1 = [...ctx, ['-', a1[1]]];
    const n2 = [...ctx, ['-', a1[2]]];
    return [n1, n2].every(n => _check(n) || tablauCheck(n));
  } else if (a1[0] === 'V') {
    const n1 = [...ctx, ['-', a1[1]], ['-', a1[2]]];
    return [n1].every(n => _check(n) || tablauCheck(n));
  } else if (a1[0] === '->') {
    const n1 = [...ctx, a1[1], ['-', a1[2]]];
    return [n1].every(n => _check(n) || tablauCheck(n));
  } else if (a1[0] === '==') {
    const n1 = [...ctx, ['-', a1[1]], a1[2]];
    const n2 = [...ctx, a1[1], ['-', a1[2]]];
    return [n1, n2].every(n => _check(n) || tablauCheck(n));
  }
  throw Error('cannot reach here', target, ctx);
}

function isTautTab (f) {
  return tablauCheck([['-', f]]);
}

function isValidInferenceTab (fs, f) {
  return tablauCheck([...fs, ['-', f]]);
}

function isEquivalentTab (f1, f2) {
  return isValidInferenceTab([f1], f2) && isValidInferenceTab([f2], f1);
}

function main () {
  const tauts = [
    'p->p',
    '(p->q)->(q->r)->p->r',
    '(p->q->r)->(q->p->r)',
    'p->q->p',
    '(p->q->r)->(p->q)->p->r',
    '((p->q)->p)->p',
  ].map(syntaxTreeOf).every(x => isTaut(x) && isTautTab(x));
  console.assert(tauts, 'taut: oops');

  const equivs = [
    ['-(pAq)', '-pV-q'], // deMorgan
    ['-(pVq)', '-pA-q'],
    ['pA(qVr)', '(pAq)V(pAr)'], // distriburity
    ['pV(qAr)', '(pVq)A(pVr)'],
    ['p-> qAr', '(p->q)A(p->r)'],
    ['p-> qVr', '(p->q)V(p->r)'],
    ['pAq ->r', '(p->r)V(q->r)'],
    ['pVq ->r', '(p->r)A(q->r)'],
    ['pAq ->r', 'p->q->r'], // deduction theorems
  ].map(p => p.map(syntaxTreeOf))
    .every(([f1, f2]) => isEquivalent(f1, f2) && isEquivalentTab(f1, f2));
  console.assert(equivs, 'equivs: oops');

  const definitions = [
    ['pVq', '-(-pA-q)'],
    ['pAq', '-(-pV-q)'],
    ['p->q', '-pVq'],
    ['p->q', '-(pA-q)'],
  ].map(p => p.map(syntaxTreeOf))
    .every(([f1, f2]) => isEquivalent(f1, f2) && isEquivalentTab(f1, f2));
  console.assert(definitions, 'fn defs: oops');

  const infer = [
    ['-q->-p', 'p->q'], // contraposition
    ['--p', 'p'], // double-negation
    ['q', 'p', 'p-> q'], // modus ponens
    ['pV-(qVr)', '(pV-q)A(pV-r)'], // bekki p49
    ['(pV-q)A(pV-r)', 'pV-(qVr)'], // bekki p49
    ['p->q->s', 'pAq->r', '-s->(t->u)', 'r->-(t->u)'], // bekki p52
    ['p', '-p->q', 'q->-r', 'rVs', '-s'], // bekki p53
  ].map(p => p.map(syntaxTreeOf))
    .every(([f, ...fs]) => isValidInference(fs, f) && isValidInferenceTab(fs, f));
  console.assert(infer, 'infer: oops');
}

main();