[HN Gopher] Recursive Program Synthesis using Paramorphisms [pdf]
___________________________________________________________________
Recursive Program Synthesis using Paramorphisms [pdf]
Author : luu
Score : 63 points
Date : 2024-07-08 18:18 UTC (5 days ago)
(HTM) web link (theory.stanford.edu)
(TXT) w3m dump (theory.stanford.edu)
| fbriggs wrote:
| Here's my paper on recursive program synthesis using combinator
| expressions from 2006:
|
| https://www.cs.hmc.edu/~oneill/papers/Combinators-ASPGP.pdf
| 082349872349872 wrote:
| I'd guess introns are also prevalent in human-synthesised
| programs?
| grugagag wrote:
| What are human-synthesised programs?
| 082349872349872 wrote:
| Ones that people manually craft/write/hack up/slap
| together...
| almostgotcaught wrote:
| Academia is about figuring out progressively fancier and fancier
| sounding names for the same mundane things.
| bubblyworld wrote:
| Expertise in any domain involves picking apart the mundane in
| progressively more complex ways! I think academia ends up with
| wild terminology because there's also the constraint of having
| to write everything down.
| almostgotcaught wrote:
| I'm an expert in this domain. People make up words for the
| sake of sexy paper titles. You can recognize it when there's
| no formal definition in the body of the paper;
|
| > paramorphisms, a class of programs that includes the most
| common recursive programming patterns on algebraic data types
|
| "most common ... patterns". ok.
|
| they're _alluding_ to math[1] but they 're not doing math.
|
| [1] https://link.springer.com/article/10.1007/BF01211391
| bradrn wrote:
| They define paramorphisms more rigorously on pages 4-5.
| almostgotcaught wrote:
| That's not at all what they define in that section. They
| define their chosen combinator that is called "para"
| which is as close to what they're alluding to as a
| bicycle is to a semi truck.
| trealira wrote:
| They didn't coin the term paramorphism. Lambert Marteens
| did in 1992 [0]. It's an extension of the concept of
| catamorphisms. These terms were invented by people
| knowledgeable about category theory [1].
|
| I also disagree with the notion that they aren't really
| doing math. It's very straightforward to derive programs
| by proving other properties of these recursive
| combinators. I would recommend reading _A tutorial on the
| universality and expressiveness of fold_ [1] as an
| example of this; folds are catamorphisms, which is why I
| bring it up.
|
| [0]: https://www.researchgate.net/publication/256269748_P
| aramorph...
|
| [1]: https://www.cambridge.org/core/journals/journal-of-
| functiona...
| almostgotcaught wrote:
| > They didn't coin the term paramorphism. Lambert
| Marteens did in 1992
|
| I literally linked that paper.
|
| > It's very straightforward to derive programs by proving
| other properties of these recursive combinators.
|
| Cool they don't do that. There's a word for being
| obliquely related: allusion.
|
| It's amazing how much benefit of the doubt CS people get.
| In math you either prove a theorem/lemma by writing it
| out in full or you... have nothing. In CS people tell
| nice stories, draw cool diagrams, write down random
| formulae and everyone is just hmm yes brilliant.
| trealira wrote:
| > I literally linked that paper.
|
| You did; I overlooked that. I don't know why you're
| implying the authors invented the term and made up the
| combinator just now, then.
|
| > Cool they don't do that.
|
| Their program is basically doing an automated version of
| what Graham Hutton did in that paper, except they rewrite
| functions using para instead of fold.
|
| Edit:
|
| > It's amazing how much benefit of the doubt CS people
| get. In math you either prove a theorem/lemma by writing
| it out in full or you... have nothing. In CS people tell
| nice stories, draw cool diagrams, write down random
| formulae and everyone is just hmm yes brilliant.
|
| You seem to have a chip on your shoulder. I don't know
| why you're telling me this.
| Twisol wrote:
| > they're alluding to math[1] but they're not doing math.
|
| So they're applying the math somebody else already put
| together? It isn't clear what your opinion is. Are you
| saying it's not valid if it's not math?
|
| Let's judge the paper by what they say they did in the
| abstract.
|
| > We show that synthesizing recursive functional programs
| using a class of primitive recursive combinators is both
| simpler and solves more benchmarks from the literature
| than previously proposed approaches.
|
| It sounds like their proposed metrics are subjective
| ("simpler") or data-oriented ("solves more ... than
| previously").
|
| > Our method synthesizes paramorphisms, a class of
| programs that includes the most common recursive
| programming patterns on algebraic data types.
|
| They're applying a pre-existing concept ("paramorphisms")
| to a problem domain where (it is implied) it either has
| not been applied before, or with a new spin.
|
| > The crux of our approach is to split the synthesis
| problem into two parts: a multi-hole template that fixes
| the recursive structure, and a search for non-recursive
| program fragments to fill the template holes.
|
| They give a novel (,it is implied) structural model for
| solving their problem using their chosen concept as their
| key contribution to the study of this problem. It is
| indirectly suggested that factoring the recursive and
| non-recursive parts apart allows them to be handled more
| effectively individually.
|
| ---
|
| Regarding your specific complaints: I do not see any
| immediate need for new math. Nor are they inventing new
| words, at least in the title or abstract. You may have
| legitimate concerns about general academic practice, but
| if you're going to levy those criticisms at this paper,
| you could do your arguments better justice than with a
| drive-by.
| Twisol wrote:
| You're correct that they aren't defining the concept of
| paramorphisms in that section -- but that's because
| paramorphisms have been present in the literature for a
| long time:
|
| > for a detailed review of paramorphisms from a formal
| perspective, see [Meertens 1992]
|
| To your original point, the title of this paper is only
| using terms ("paramorphisms", "recursive", and "program
| synthesis") that are decidedly _not_ novel.
|
| For the benefit of other readers:
|
| As to why "paramorphisms" are singled out as a concept
| worthy of having their own name, I recommend the 1991
| paper "Functional Programming with Bananas, Lenses,
| Envelopes and Barbed Wire" by Meijer, Fokkinga, and
| Paterson, which is much more readable than the referenced
| Meertens paper.
|
| We all know what an "infinite loop" is; a natural
| question is whether there are any looping constructs that
| cannot get caught in an infinite loop. The "for-each"
| loop has become popular in imperative languages; the
| reason it works is because it does a kind of _structural
| iteration_ over finite data which fits a regular pattern.
|
| A "catamorphism" precisely captures this notion of
| structural iteration (really, structural _recursion_ ),
| for a vast family of data types (the "inductively
| defined" ones). But for any algorithm where you'd use an
| unbounded loop (or unbounded recursion), it's not always
| easy (or possible!) to implement that algorithm using
| catamorphic recursion instead -- and they're not always
| the most performant, either (e.g. you can't short-circuit
| the recursion).
|
| So we've gone from something that is too
| powerful/expressive (unbounded recursion/iteration) to
| something that is not powerful/expressive enough
| (catamorphic recursion/iteration), with the dividing line
| of "allows infinite loops" somewhere in the middle. The
| study of general recursion schemes, which includes
| paramorphisms, is essentially the study of alternatives
| to unbounded recursion/iteration that are better than
| catamorphisms on one or more desiderata.
| almostgotcaught wrote:
| > present in the literature for a long time:
|
| You're the second person to link the exact same paper I
| did in my first response.
|
| > To your original point, the title of this paper is only
| using terms ("paramorphisms", "recursive", and "program
| synthesis") that are decidedly not novel.
|
| They italicize paramorphism in the abstract. We all very
| well know that italics means novel usage. So again: let's
| drop the charade that everything is above board here.
| trealira wrote:
| > They italicize paramorphism in the abstract. We all
| very well know that italics means novel usage.
|
| Or, they're writing for an audience that isn't
| necessarily familiar with paramorphisms and other
| morphisms, but still is familiar with functional
| programming.
| Twisol wrote:
| > You're the second person to link the exact same paper I
| did in my first response.
|
| Yes; it _sounds_ like you 're suggesting they should be
| defining these concepts themselves instead of saying
| somebody else did them. But that would be academic
| dishonesty. So you must be alluding to something else.
|
| > We all very well know that italics means novel usage.
|
| You say that as though expecting everyone to agree. I do
| not. I personally use italics because several people I
| have spoken with, including my advisor, feel that
| boldface is shouty. Underline is rarely used for a
| similar reason. Italic font is the the only available
| form of typographic \emph{asis}; it is used (if
| sparingly) for key terms and ideas that the reader's
| attention should be drawn to, which _include_ novel
| ideas, but can be much more than that.
| gergo_barany wrote:
| > let's drop the charade that everything is above board
| here.
|
| OK. Since you're opposed to merely _alluding_ to things
| (your italics, which I find funny), could you please
| state explicitly the misconduct you are alleging?
| bubblyworld wrote:
| Mmm, yeah on reading the paper more closely it seems like
| they don't make essential use of the concept really. It's
| more of a descriptor of the mechanics of their combinator
| language.
|
| Personally I'm fine with that - I have no issue with CS
| people borrowing terminology from category theory to
| describe stuff, so long as the analogy is reasonable. But I
| get where you're coming from - having learned some CT in
| (grad) school, I used to find Haskell wikis confusing as
| heck because they use CT terminology but nobody clarifies
| what category they're actually working in!
| tome wrote:
| > I used to find Haskell wikis confusing as heck because
| they use CT terminology but nobody clarifies what
| category they're actually working in!
|
| "Hask", the (almost) category where the objects are types
| and the morphisms from A to B is the type A -> B.
| bubblyworld wrote:
| Thanks, I know that now, but it's the "almost" part that
| trips up people like me! And it's not helped by the fact
| that the same sources will say something like "a monad is
| a monoid in the category of endofunctors", yet if you
| take Hask seriously there should be a discussion of
| endofunctors on Hask etc. When details are missing my
| brain gets stuck on figuring them out (whereas for
| Haskell the right approach is to take it with a pinch of
| salt and move on I think).
|
| Edit: to be more specific, you need to specify what
| constitutes a type - all possible ADTs under all possible
| names? Are equivalent functions considered the same
| morphism? What about seq? Is there a privileged "IO"
| type, and if not how is it represented in the set of
| types? What about other monads hiding different side
| effects? What about bottom? Many of these choices will of
| course be equivalent in some sense, but technically
| speaking you don't have a category until you've nailed
| this stuff down.
___________________________________________________________________
(page generated 2024-07-13 23:02 UTC)