Even more puzzling to me is how you can consider unary addition to be isomorphic to binary addition. I am no bisimulation expert but unary addition involves a single state change whilst binary addition requires many.
I will have to drop out of the debate, yet again, with the feeling we are living in completely different worlds.
Oh, I think that ship sailed long ago. This started as a discussion on Kotlin. :)
> The point is that fac1 and fac2 do two completely different things when executed on a computer.
But they don't. You must define some equivalence relation to determine whether executions are "completely different". You could go very concretely, all the way down to memory addresses or even to logic gates in the CPU, but then the very same Haskell program may be considered to be completely different from itself when compiled by different compiler versions. So, when working with powerful systems like TLA, you get to decide how fine-grained your equivalence is, but when talking about programs and languages, you go by the semantics of the language and use (bi)simulation, as it's the homo/isomorphism normally used in programming language theory (it was first proposed, I believe, by Robin Milner). Such an isomorphism exists between the things those programs do in the computer.
> Even more puzzling to me is how you can consider unary addition to be isomorphic to binary addition. I am no bisimulation expert but unary addition involves a single state change whilst binary addition requires many.
Because you are allowed to map a single state in one graph to multiple ones in the other. That's the difference between a function and a relation.
> I will have to drop out of the debate, yet again, with the feeling we are living in completely different worlds.
Well, all I can say is that this particular branch of the discussion began when I pointed out that the functional denotation is one particular choice, made to obtain certain tradeoffs, while others, with other tradeoffs, exist. If by your world you mean the world when you only consider the theory of functional programming, then indeed there's no point discussing it within the broader context of programming language theory/program analysis. Afer all, the theory of functional programming is a strict subset of programming language theory. I don't know how to compare FP to itself, nor do I know how to compare the mathematics of FP to some imprecise notion of imperative programming. I can try to compare the mathematics of FP to the mathematics of imperative.
Functional programmers care about all sorts of semantics, including operational and denotational semantics. I see no reason the sorts of analysis you give in your Java examples couldn't equally be applied to functional programs not least because functional programs can be trivially rewritten as imperative ones (see CBPV).
Oh, but that's because FP fans call it "referential transparency"; I'm sure you've come across that term. While the terminology is incorrect (for one, Java is also referentially transparent), when FP fans say "referential transparency", they mean "value semantics", i.e., that the meaning of a function application is its normal form, or, in other words, they simply mean "functional denotation". This is exactly what enables the equational reasoning FP fans like to talk about.
> I see no reason the sorts of analysis you give in your Java examples couldn't equally be applied to functional programs
They could (I know it's possible to write assertions in Haskell), but then they no longer operate on the denotation of the language. You can also use unsafePerformIO in Haskell, but if you do that, you may break the mental model the language aims to create.
> not least because functional programs can be trivially rewritten as imperative ones (see CBPV).
Again, they could, but not in a way that preserves the benefits for which the formalism was designed for. Similarly, pure functional programs could be written in Java, but that's not the idiomatic way.
To take us back to where we started, we are talking about language design, and while many languages can imitate the style of others, they are optimized for certain pragmatic and aesthetic concerns. That is my whole point.
If that were your whole point we could have avoided this thread. No one disputes that.
In fact your point seems to be that Java/imperative languages are better than Haskell/functional languages, for a reason that you have tried to elaborate and that I have failed to understand.
Not at all. My point is that the reason for preferring a formalism is largely aesthetic and pragmatic, and almost never mathematical or universal. Indeed, one pragmatic reason to prefer classical imperative programming is that in many cases, it makes formal reasoning easier, something that comes as a surprise to those familiar with the math of FP but not of imperative (you don't have to take my word for it; here are Xavier Leroy and Simon Peyton Jones saying that: http://homepages.inf.ed.ac.uk/stg/Milner2012/Monday_Panel-ht...).
But if you knew me you'd know that I don't care much for programming languages at all, partly because personally I don't feel much of a difference and partly because the empirical evidence so far show that there is little if any practical difference between them (at least modern ones). So I resist any attempt (by lmm this time) to claim that functional languages are "better designed" because of one or other of their properties. They are not, but they may be languages that lmm or you find aesthetically appealing, and more productive because they match how you like to think about programs.
I'm skeptical of all languages, but I am at least hopeful of languages that haven't yet had the chance of proving themselves, which is why I'm curious about Eve, the most theoretically-advanced language that I know of, and one whose semantics I personally find appealing (actually, some of the ideas behind Eve have proven themselves quite spectacularly in realtime, which is why I'm even more hopeful).
First, operational semantics is usually a state machine (e.g., in the case of lambda calculus, the current expression is the state and the reductions are transitions). Second, there is no a-priori requirement that mapping the states of two state machines preserve complexity. You can add this restriction if you want to show they have the same complexity (as in polynomial reduction when showing membership of complexity classes), but that's an additional constraint.
> It is the denotational semantics whose notion of meaning is the "end result of the computation".
No. That's just the functional denotational semantics (i.e., the matehmatical meaning of a program is a so-called "partial function", which resembles a function). Imperative programs can have a Hoare-logic denotation (which I used in my Java example). TLA has a behavior denotation (the mathematical meaning of a program is a set of its possible behaviors, where a behavior is an infinite sequence of states, where a "terminating" computation is defined to be one where some state is reached in a finite number of steps, and then "stutters" forever). A language such as Eve can use a denotation where every block is a relation on the current and next state, and the entire program is such a relation, made by intersecting all blocks.
> No, not at all. In fact let's make it simpler: I wouldn't even consider addition of unary integers to be operationally isomorphic to addition of binary integers.
Well, in program analysis, the ordinary (homo/iso)morphism between programs is the (bi)simulation relation, and in this case the two are isomorphic.
> Denotationally they're the same, of course.
No, again, this depends on what your denotation is. In Haskell, for example, even two instances of Euclid's algorithm using a binary representation may not be denotationally equivalent, as in my example, but in TLA, for example, they would be.
> yes, I consider the "Euclid's algorithm" part of "Euclid's algorithm operating on unary integers" to be the same as the "Euclid's algorithm" part of "Euclid's algorithm operating on binary integers"
Ah, and the simulation relation (or the much nicer refinement relation in TLA) precisely and mathematically captures the notion of what it means for two programs to implement the same algorithm. In TLA, A => S and B => S iff A and B implement the same algorithm S. I.e., in TLA, you have a very simple and precise operator that defines the notion of abstraction.
> I'm not especially familiar with the notion of bisimulation but if you can demonstrate that the addition of unary integers is bisimilar to the addition of binary integers then I would be very interested!
Picture a graph where each node is the state of the computation, and the edges signify transitions. If you want to think in terms of LC, the state can be some lambda expression, and the transitions are reductions. In the case of deterministic programs with a fixed input (let's say that we're only considering the computation of factorial(5)), it's a linear graph. There is a subtlety here, as the lambda calculus does not specify a reduction order and so creates a non-linear graph, with different paths representing different reduction orders. But normally, programming languages come with an evaluation strategy, a state machine, that accompanies the LC (by-name for Haskell, by-value for ML).
BTW, if we label each node with the set of all atomic propositions that are true in that state, we get what is known as the Kripke structure of the program, which is the canonical program representation in all of program analysis.
A simulation relation is a relation from program A to program B that maps states to states and transitions to transitions, such that for every transition that A makes, B can match it with a mapped transition that leads to a mapped state. If the relation is invertible, we say that it's a bisimulation, and it forms an isomorphism on programs. You can see that whether you label the states with a number in unary or in binary, the graph is the same, so clearly an invertible relation exists.
See Wikipedia for a more precise treatment: https://en.wikipedia.org/wiki/Bisimulation
If you want, you can place further restrictions on the mapping, such as bounding its complexity to show tighter similarity. Here I show how you can describe an actual lattice relating programs to one another: https://pron.github.io/posts/tlaplus_part4#equivalence-abstr... The following section (which does not require any previous knowledge of TLA), specifically discusses (bi)simulation: https://pron.github.io/posts/tlaplus_part4#other-notions-of-...