2008/08/07

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) → RP 是 positive 但不是 strictly-positive。至於 positive/negative occurrence 會造成什麼影響還要再看一看。

不乖乖讀一點課本還是不行啊 XD。

--
而且難得有一本要看的書是買得到的 XD。

Labels:

Anonymous scm8/08/2008 5:45 pm 說:

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 哩?需要反函數呢。 :)

 

<< 回到主頁