関係概念を使った整理

含有関係と出現関係について述べる。

まず関係型の定義：

reltype contains : Item +-> Item
reltype containedIn := contains^t
reltype occursIn : Term +-> Item
reltype hasOccurrence := occursIn^t

オーバーロードした定義：

reltype (_1 contains _2 at _3'): i:Item, Range(i) +-> Item
reltype (_1 containedIn _2' at _3') := contains^t : Item +-> i:Item, Range(i)
reltype (_1 occursIn _2' at _3'): Term +-> i:Item, Range(i)
reltype (_1 hasOccurrence _3' at _2) := occursIn^t : i:Item, Rnage(i) +-> Term

関係の制約条件：

(_ hasOccurrence _ at _) : PartialFunction(i:Item, Rnage(i) +-> Term)
(_ contains _): PartialFunction(i:Item, Range(i) +-> Item)

推論規則：

x occursIn i at p , i contained j at q ⇒  x occursIn j at q/p
x occursIn i ⇔ ∃p:Pos(i).( x occursIn i at p)

制約条件や推論規則の解釈は集合論と古典述語論理を使う。