$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2008/05/03

### 馬賽克

• 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.

--

Labels:

Anonymous5/03/2008 12:00 pm 說：