Positive Occurrence
從很久以前就一直模模糊糊搞不清楚的 "positive/negative occurrence" 剛剛終於在《Types and Programming Languages》（Google 線上版 XD）找到精確的定義，的確就是 scm 老師講的「箭頭的左邊」。這樣的說法來自古典邏輯的
P → Q ⇔ ¬P ∨ Q所以
P 是在 "negative" 的位置，Q 在 "positive" 的位置。至於 "strictly-positive" 排除的是 "doubly-negative" 的情形，例如 (P → Q) → R 的 P 是 positive 但不是 strictly-positive。至於 positive/negative occurrence 會造成什麼影響還要再看一看。
不乖乖讀一點課本還是不行啊 XD。
--
而且難得有一本要看的書是買得到的 XD。
Labels: Type Theory
Hmmm.. 舉例吧。比如，考慮 F X = A -> X. 當 X 越大，F X 也越大。但如果是 F X = X -> A, X 越大，F X 反而越小。
取 fixed-point 通常的基本條件都是 F 要 monotonic. 所以有 X 只能出現在 strictly positive 位置的限制。如果要處理 general 的情況好像也是可以，不過就更複雜了。
另外一個現象，當 F X = A -> X, mapF 還蠻好定的：
mapF : (a -> b) -> (A -> a) -> (A -> b)
mapF f g = f . g
如果 F X = X -> A, 要怎麼定 mapF 哩？需要反函數呢。 :)
<< 回到主頁