大久保弘崇
ex10.4
最終更新：
hirotakaohkubo
-
view
10.11
instance ArrowLoop StreamMap where
loop (SM f) = SM (trace (unzipStream . f . zipStream))
10.12
| loop (first f) | |
| = loop (first f >>> idA) | {恒等性} |
| = f >>> loop idA | {左結合} |
| = f >>> loop (pure id) | {定義} |
| = f >>> pure (trace id) | {拡張} |
| = f >>> pure id | ※ |
| = f | {定義と恒等性} |
※部
| trace id | |
| =λb → let (c,d) = id (b, d) in c | {定義} |
| =λb → b | |
| = id |
10.13
考え中。
10.14
pはパターン、aは複雑な式、fはアロー式。
いずれの形も使えるということから、
いずれの形も使えるということから、
- FV(p) と FV(f) は disjoint
- このアローはArrowApplyのインスタンス
である。
１つめを使う場合。
proc p → f -< a = pure (λp→a) >>> f
proc p → f -< a = pure (λp→a) >>> f
２つめを使う場合。
aはpに依存するが、fは依存していないことから、
λp→(f,a) = (λc→(f,c)) . (λp→a)
がいえる。
aはpに依存するが、fは依存していないことから、
λp→(f,a) = (λc→(f,c)) . (λp→a)
がいえる。
| proc p → f -< a | |
| = pure (λp → (f,a)) >>> app | {定義2} |
| = pure (λc→(f,c) . λp→a) >>> app | {上} |
| = pure (λp→a) >>> pure (λc→(f,c)) >>> app | {関手合成} |
| = pure (λp→a) >>> mkPair f >>> app | {定義} |
| = pure (λp→>a) >>> f | {外延性} |
10.15
http://www.soi.city.ac.uk/~ross/papers/notation.html にcaseの話も込みで全部書いてある。
proc p → if e then c1 else c2 = arr (λ p → if e then Left p else Right p) >>> (proc p → c1) ||| (proc p → c2)
しかし、変換を完全にするには、
proc p → { if e then c1 else c2 ; B }
を対象にするか、またはこれが
proc p → if e then proc p → { c1 ; B } else proc p → { c2 ; B }
に変換できることを示せないと不充分ではないか。
proc p → if e then c1 else c2 = arr (λ p → if e then Left p else Right p) >>> (proc p → c1) ||| (proc p → c2)
しかし、変換を完全にするには、
proc p → { if e then c1 else c2 ; B }
を対象にするか、またはこれが
proc p → if e then proc p → { c1 ; B } else proc p → { c2 ; B }
に変換できることを示せないと不充分ではないか。
