You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Ryan Schwiebert (Sep 17 2024 at 03:08):I ran across the term "Futamura projection" when reading souffle-lang's site.
http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html
While the atmosphere is crackling with category-theoretic energy, I actually can't find sources that discuss the connection.
Can anyone couch the concept of Futamura projections in terms of category theory? I have a feeling it'll make it faster for me to understand...
fosco (Sep 17 2024 at 09:00):I honestly read "futurama projections" three times before noticing that no, that's not what's written
fosco (Sep 17 2024 at 09:03):This being said: the thing that comes to mind when reading that one can "stuff a description of a specialiser into the specialiser's own first input" is Lawvere's fixpoint theorem, survey'd here https://arxiv.org/abs/math/0305282
And probably this is corroborated by the previous remark that this is all about machines making machines (so, whatever category you can encode this in, will have internal homs)?
fosco (Sep 17 2024 at 09:04):(I have no precise idea what I'm talking about, of course)
Ryan Schwiebert (Sep 17 2024 at 11:36):Huh: I never would have thought to see "fixed point theorems" grouped with "paradoxes and incompleteness theorems". Interesting!
John Baez (Sep 17 2024 at 15:38):See
A quine is a computer program that takes no input and produces a copy of its own source code as its only output. The standard terms for these programs in the computability theory and computer science literature are "self-replicating programs", "self-reproducing programs", and "self-copying programs".
A quine is a fixed point of an execution environment, when that environment is viewed as a function transforming programs into their outputs. Quines are possible in any Turing-complete programming language, as a direct consequence of Kleene's recursion theorem.
John Baez (Sep 17 2024 at 15:43):Also see Quine's presentation of the Liar paradox and Goedel's first incompleteness theorem in terms of quining:
In an effort to clear up this antinomy it has been protested that the phrase 'This sentence', so used, refers to nothing. This is claimed on the ground that you cannot get rid of the phrase by supplying a sentence that is referred to. For what sentence does the phrase refer to? The sentence 'This sentence is false'. If, accordingly, we supplant the phrase 'This sentence' by a quotation of the sentence referred to, we get: ' 'This sentence is false' is false'. But the whole outside sentence here attributes falsity no longer to itself but merely to something other than itself, thereby engendering no paradox.
If, however, in our perversity we are still bent on constructing a sentence that does attribute falsity unequivocally to itself, we can do so thus: ' ' Yields a falsehood when appended to its own quotation' yields a falsehood when appended to its own quotation'. This sentence specifies a string of nine words and says of this string that if you put it down twice, with quotation marks around the first of the two occurrences, the result is false. But that result is the very sentence that is doing the telling. The sentence is true if and only if it is false, and we have our antinomy.
John Baez (Sep 17 2024 at 15:54):I'll admit I'm confused about the precise relation between Quine's original trick - ' ' Yields a falsehood when appended to its own quotation' yields a falsehood when appended to its own quotation' - and fixed point theorems. What's the map that has a fixed point here?
On the other hand, it seems the modern computer science use of "quine" is different: it's a program that yields itself as output, so it's a fixed point of evaluation. For a proof that any Turing complete language has such a fixed point, try this:
Maybe the two uses of "quine" are more connected than I realize.
Bruno Gavranović (Sep 17 2024 at 16:42):@Ryan Schwiebert, I often wonder about this question too.
Some time ago I came across this particularly compelling graphical calculus for composing compilers.
image.png
While I'm not sure if it says anything related to Futamura projection in particular, it seems highly relevant.
Some of the high-level algebra is reminiscent of the algebra of composing maps with the para construction too
Amar Hadzihasanovic (Sep 18 2024 at 08:26):@dusko presents the Futamura projections in terms of "monoidal computers" in Section 6.2.2 of his book.
Mike Stay (Sep 19 2024 at 05:24):The linked blog post talks about specializers, which fix an input and then optimize the resulting program. But optimization of internals is deeply related to the execution of programs, which denotational semantics largely ignores. So if there is a nontrivial categorical view of the Futamura projections, it will have to be in a context where we can model programs evolving over time. The Lambek & Scott approach to interpreting lambda calculus in a CCC won't suffice: the morphisms are beta-equivalence classes of terms with one free variable, but the number of beta reduction steps is precisely what the optimizer is attempting to reduce.