### 馬賽克

看看我現在能把 scm 老師去年 derivation 投影片裡面的馬賽克去掉多少 XD。

- p.6: ... (which could be non-executable, e.g., relational specifications) ...
- p.10: For the purpose of this lecture, we regard functional programs as arrows in the category
**Fun**, i.e., total functions between sets. The reality is more complicated and we may need to move to**Cpo**or even**Rel**taken as a (tabular, unitary, locally-complete, power, ...) allegory. (Then proceed with the formal definition of a category.) - p.11:
`fact`

is the least fixed point of the equations above. In fact, since`fact`

is a paramorphism, which is defined in terms of catamorphisms (and products), it is uniquely defined. - p.12: Noticed some similarities? Their constructors are both initial algebras with base functors X ↦ 1 + X and X ↦ 1 + A × X, respectively.
- p.17:
`map`

is the type functor for lists. - p.26: One can also prove the fact by fold-fusion.
- p.28:
`sum . concat = sum . map sum`

is called the bookkeeping law in Bird's*Introduction to Functional Programming using Haskell*. - p.29: (Derive the induction principle from the universal property of catamorphisms.)
- p.32: Fold-fusion.
- p.40: Fold-fusion.
- p.43: Write
`steep = fst . <steep, sum>`

then apply Fokkinga's mutual recursion theorem. - p.52: One way to look at
`foldr (⊕) e`

is that it replaces`[]`

with`e`

and`(:)`

with`(⊕)`

, because a catamorphism is a homomorphism from the initial F-algebra to some F-algebra. - p.52:
`id = foldr (:) []`

is the reflection law. - p.58: Derive the fold-fusion theorem from the general fusion law.
- p.61: Fusing a function into
`id`

is just exploiting the universal property of catamorphisms. - p.61: Since we are working under
**Fun**and do not emphasise constructivity, we have a theorem giving a necessary and sufficient condition for deciding when a function is a fold (or an unfold). - p.69: Naturality, bookkeeping law, functor, monotonicity, and tupling.
- p.83: Folds and unfolds are exactly dual concepts. The former are homomorphisms from initial F-algebras to F-algebras, while the latter are homomorphisms from F-coalgebras to final F-coalgebras.
- p.85: Do the coinductive proof by unfold-fusion.
- p.98: Or we can move to
**Rel**, where initial algebras and final coalgebras coincide, and partiality and nondeterminism can be elegantly dealt with. (Another 100 pages to explain all the terms.) - p.101: Read Bird and de Moor's
*Algebra of Programming*.

--

從這份投影片我了解到「什麼東西不要放進去」恐怕比「什麼東西要放進去」還更重要而且更困難 XD。

Labels: FLOLAC '07

推薦你看賴聲川的創意學:p

<< 回到主頁