定義が良く分からないので...

ここ3日ぐらいちょいちょいと読んでいるRalph Matthesさんの論文全然分からない所があるのではてなさんに纏めてみます。
つまりぼくでは分からない過ぎるので、分かる人に教えて貰いたいという事なのですが...。

MatthesさんのInductive Typesを扱った論文では(strictly)positiveな出現の定義がどれも書かれているのですが、その定義がどうも良く分からんという事です。

例としてその中でもシンプルそうな「strictly positive」な定義に関する部分を、氏の論文「Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types」(http://www.irit.fr/~Ralph.Matthes/works.html)から抜き出します。

Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types p45より

Inductively define the set SPosTypes of strictly positive types(as a subset of Types) and simultaneously for every ρ ∈ SPosTypes the set SPos(ρ) of type variables which only occur free at strictly positive positions in ρ:

(V) α ∈ SPosTypes and SPos(α) := Typevars.
(→) If ρ ∈ SPosTypes and σ ∈ SPosTypes,then ρ → σ ∈ SPosTypes and SPos(ρ → σ) := SPos(ρ)＼FV(ρ).
(∀) If ρ ∈ SPosTypes,then ∀αρ ∈ SPosTypes and SPos(∀αρ) := SPos(ρ) ∪ {α}
...(残り省略)

Typevarsは型変数と見なせるシンボルの無限集合　で　Vに関しては

同論文 p9 より
(V) If α ∈ Typevars,then α ∈ Types

となっています。

しかし、この定義だと例えば

SPos(α) = Typevars (しかし、普通これは {α} となるのでは?)
SPos(∀α.α) = Typevars (αは束縛出現なのではないか?)

という感じでどうもしっくり来ません。

いや、しっくり来るとかは私の中の問題なのですが・・・。

positiveとnegativeの定義は、TAPLのp428とかに書いていて、どうもその定義と比べるとなんだろううーん違うんじゃ無いですか？というのでどうしてこういう定義にしたんだろう。

(TAPLの該当ページ http://j.mp/dlo5Td)

他の文献

Basic Proof TheoryのIntroductionあたりに色々書いてるのを発見 http://j.mp/d9QtLN

そもそもMatthesさんの論文は、SPosとかPosとかNegがif側に出て来ているのはμ-ruleだけだなー

意味が分かったかも

「そもそもMatthesさんの論文は、SPosとかPosとかNegがif側に出て来ているのはμ-ruleだけだなー」という所だけに注目すると、むしろSPos(ρ)というのはρの中でstrictly positiveな出現を破っていないものの集合という事になるのではないかしら?