Ezra's Research

So I got sucked into editing the wikipedia page for anamorphisms, which was a mess: it didn't define the concept itself, except to say that it's a generalization of unfolds, and allude to category theory; it had duplicated code, but treated the duplicates as different, and was generally jargon-heavy and not very helpful.

But while fixing it, I got stuck on a puzzle: what exactly is an anamorphism?

Is an anamorphism a higher-order unfold operator? Or is it any function which is defined by partially applying such an operator? Or a function that is defined using a certain syntactic pattern, corresponding to an unfold operator? Or any function at all that could be so defined?

In the almighty "Programming with Bananas, Lenses, Envelopes and Barbed Wire," they seem to use "anamorphism" to refer to a function defined by a certain syntactic pattern. It's a question of interpretation, but they don't seem to define it as a higher-order function, exactly: the text posits some pre-existing operators and then the code sample, which takes just one argument (the "seed" value to unfold from), uses those posited operators.

It seems natural to me to use "anamorphism" to refer to the (unique) unfold operator for a given ADT, and likewise for "catamorphism" and fold. We still have the plural "anamorphisms," since we have many types with such operators. And, I'm not sure to what extent a function is intrinsically "an anamorphism" in Meijer, et al.'s sense. Of course, it is intrinsic whether a function can or cannot be defined that way; but when we start using the whole bag of bananas, lens, envelopes and barbed wire, I think we get multiple ways to define many functions, so it's less intrinsic.

I'd like to hear what others think: What are anamorphisms? Please comment!

Posted by Ezra elias kilty Cooper at 5:26 AM | Permalink | Comments (3)

I've been working on trying to extend a result from my thesis, having to do with strong normalization of a certain higher-order rewrite system, but its proof is very complicated, so I've been working on simplifying it.

Along the way I found a paper by Mitsuhiro Okada from 1989 which proves strong normalization for the combination of STLC with any first-order term-rewriting system. But this paper is hard to read because it has strange notations and concepts and says things like, "If a part s[*/x1, ..., */xn, */y] of t belongs to the cap then the part s[*/x1, ..., */xn, */y] also belongs to the cap." Say what?

I knew I could prove the same result using the Tait-Girard method (the same basic approach Okada takes) in a more straightforward way—at least to me. So I did, and here it is for future reference: "Simply adding lambda won't make your rewrites diverge."

Posted by Ezra elias kilty Cooper at 2:54 AM | Permalink