馬賽克

看看我現在能把 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。

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