日々の流転

λ. When is a function a fold or an unfold?, Jeremy Gibbons, Graham Hutton, and Thorsten Altenkirch

を読んだ。集合の圏の場合の、関数がfold/unfoldの形で書けるための必要十分条件を与えている。証明は集合論的かつ選択公理を使っているので、構成的な関数の圏に一般化することは出来ない。条件とその証明は非常にシンプルなんだけど、具体例はちょっと不思議な感じもする。

• (∃g:FA->A. h = fold g) ⇔ ker(Fh)⊆ker(h ∘ in)　*1
• (∃g:A->FA. h = unfold g) ⇔ img(Fh)⊇img(out ∘ h)

λ. Constructively Characterizing Fold and Unfold, Tjark Weber and James Caldwell

.