Wiki

古典論理シーケント計算

一般に，代数仕様からは項書換え系と呼ばれる実行環境が生成される．しかし，それにはいくつかの制限がある．例えば，次のような等式のように，等式の右辺や条件式に，等式の右辺に現れない変数が出現しているようなものは，項書換え系に反映されない．

そこで，ここでは，CafeOBJで古典論理シーケント計算LKを部分的にシミュレートするためのモジュールを紹介する．シーケントを用いれば，等式の右辺，左辺，条件式を１つの項として宣言できるので，上に上げた制限は若干改善される．

#!python

    cq l(x) = r(x,y) if p(x,y,z)

PROPとPROPS

PROPは，命題を表すモジュールである． CafeOBJ処理系による簡約が意図を超えて行われることを防ぎ，適宜拡張ができるように，真理値を表す内蔵モジュールBOOLを拡張して定義している

#!python
module PROP
{
  signature
  {
    [ Bool < Prop ]
    op _and_ : Prop Prop -> Prop { assoc comm }
    op _or_ : Prop Prop -> Prop { assoc comm }
    op not_ : Prop -> Prop
    op _implies_ : Prop Prop -> Prop
    op _iff_ : Prop Prop -> Prop
  }
  axioms
  {
    vars P Q R : Prop
    eq false and P = false .
    eq true and P = P .
    eq P and P = P .
    eq true or P = true .
    eq false or P = P .
    eq P or P = P .
    eq not true = false .
    eq not false = true .
    eq not not P = P .
    eq P implies true = true .
    eq false implies P = true .
    eq P implies P = true .
    eq P iff Q = (P implies Q) and (Q implies P) .
  }
}

PROPSは，命題の集合を宣言するモジュールである

#!python

make PROPS
(
  SET(PROP { sort Elt -> Prop }) * { sort Set -> Props }
)

SEQUENTとSEQUENTS

SEQUENTは，古典論理シーケント計算LKにおけるシーケントをソートSequentの項として定める．但し，このモジュールで定めるシーケントには，命題しか現れない．シーケントのturnstyle（├ ）の左右に置かれるのは命題の集合としている．これで，命題の配置を変える推論規則や重複する命題を除く推論規則を陽に記述せずに済む．

#!python

module SEQUENT
{
  imports
  {
    pr(PROPS)
  }
  signature
  {
    [ Sequent ]
    op _|-_ : Props Props -> Sequent
  }
  axioms
  {
    vars P : Prop
    vars L R : Props
    eq true,L |- R = L |- R .
    eq L |- R,false = L |- R .
    eq false,L |- R = false |- R .
    eq L |- R,true = L |- true .
  }
}

SEQUENTSはシーケントの集合を表すモジュールである．

#!python

make SEQUENTS
(
  SET(SEQUENT{ sort Elt -> Sequent }) * { sort Set -> Sequents }
)

JUDGEMENT

JUDGEMENTは，シーケントの真偽を判定するためのものである．

#!python

module JUDGEMENT
{
  imports
  {
    pr(SEQUENTS)
    pr(RWL)
  }
  signature
  {
    op hold : Sequents -> Bool
    op hold : Prop -> Bool
  }
  axioms
  {
    vars P Q : Prop
    vars L R : Props
    vars S T : Sequents
    eq hold(nil |- nil) = false .
    eq hold(L |- true) = true .
    eq hold(false |- R) = true .
    eq hold(P,L |- R,P) = true .
    cq hold(L |- R,P) = true
       if hold(L |- R) = true .
    cq hold(L,P |- R) = true
       if hold(L |- R) = true .
    eq hold(nil) = true .
    eq hold(S,T) = hold(S) and hold(T) .
    cq hold(P) = true
       if P = true .
    cq hold(P) = true
       if hold(nil |- P) =(1,*)=>* true .
  }
}

JUDGEMENTで宣言されている演算holdは，与えられたシーケントが正しいか否かを計算する．弱化（weakning）規則は，ここで宣言した条件付き等式に含まれる． holdは，シーケントの集合上の演算に拡張される．任意の集合Sに対するhold(S)の値は，Sに属する全てのシーケントqが真であれば，すなわち，hold(q)が真であれば，真となる．また，holdは命題上の演算としても宣言される．与えられた命題Pに対してシーケント ├ P を真に書換えることができるとき， hold(P)の値は真になる．

INFERENCE

モジュールINFERENCEでは，推論は項で表される．

#!python
module INFERENCE
{
  imports
  {
    ex(JUDGEMENT)
  }
  signature
  {
    [ Inference ]
    op antecedent : Inference -> Sequents
    op consequent : Inference -> Sequents
    op derivable : Inference -> Bool
  }
  axioms
  {
    vars I : Inference
    cq derivable(I) = true
       if antecedent(I) =(1,*)=>* consequent(I) .
    cq hold(consequent(I)) = true
       if derivable(I) and hold(antecedent(I)) .
  }
}

演算antecedentは与えられた推論の前提，すなわち，規則を適用される前のシーケントの集合を返し，演算consequentは与えられた推論の結論，すなわち，規則を適用された後のシーケントの集合を返す．前提から推論に（定められた規則のみ適用して）書換えられる場合，その推論はderivableであるといい，正しい前提からdelivableな推論を通して導かれる結論は，やはり正しいとみなされる．

RULE

モジュールRULEでは，推論規則を書換規則で宣言している．

#!python
module RULE
{
  imports
  {
    pr(SEQUENTS)
  }
  axioms
  {
    vars P Q : Prop
    vars L R : Props
    vars S T : Props
    rl (L,P |- R),(S |- P,T) => L,S |- R,T .
    rl L,P |- R => L |- (not P),R .
    rl (L |- P,R),(S |- Q,T) => L,S |- (P and Q),R,T .
    rl L |- P,Q,R => L |- (P or Q),R .
    rl L |- (P or Q),R => L |- P,Q,R .
    rl L,P |- Q,R => L |- (P implies Q),R .
    rl L |- P,R => L,(not P) |- R .
    rl L,P,Q |- R => L,(P and Q) |- R .
    rl L,(P and Q) |- R => L,P,Q |- R .
    rl (L,P |- R),(S,Q |- T) => L,S,(P or Q) |- R,T .
    rl (L |- P,R),(S,Q |- T) => L,S,(P implies Q) |- R,T .
  }
}

ここで宣言されている規則は，カット，否定の導入，論理積の導入，論理和の導入，含意の導入である．

LK

LKは，上に挙げたモジュールの和をとったものとなる．

#!python

make LK
(
  INFERENCE + RULE
)