I've always wondered if there's more to FP than (more or less) point-free style with an associated algebra. TFA seems to stop just when it might get interesting. Did Backus ever develop (or aim for) a notion of semantic completeness, e.g. Cartesian closure or whatever works [0] for Hughes's Arrows? The last has the interesting property of being foundationally point-free but also supporting a syntax with variables (with non-standard scoping rules). Which perhaps refutes Backus's original concerns.
Your comment blows my mind a bit. Of course we do! Here I am, having decided to blithely parade my ignorance here without any concern whatsoever for what is relevant (what the implications may be) ...
... but on the other hand I think you're saying that we can never fully account for all the relevant stuff or what it entails for any number of reasons, not the least being that we don't know (and can't know) what all the consequences are.
And yet we still need to make decisions, and winnow what we base those on.
The intro to TFA> To most AI researchers, the frame problem is the challenge of representing the effects of action in logic without having to represent explicitly a large number of intuitively obvious non-effects. But to many philosophers, the AI researchers' frame problem is suggestive of wider epistemological issues. Is it possible, in principle, to limit the scope of the reasoning required to derive the consequences of an action? And, more generally, how do we account for our apparent ability to make decisions on the basis only of what is relevant to an ongoing situation without having explicitly to consider all that is not relevant?
Near as I can tell separation logic (suitably generalised/tamed/adapted to suit the system of interest/tools in use) addresses all these concerns. I'm not claiming it solves every last variant of the frame problem that anyone has ever considered; just that it seems to address the classical concerns about modularly specifying the effects of actions.
Take, for instance, the last question: separation logic models this by explicitly splitting the state (of the system of interest) into "relevant" and "not relevant" via separating conjunction (etc) and the suggestively-named "Frame" axiom takes care to preserve the "not relevant" part.
This partially addresses epistemics too, but I see that an action may affect things that I am not aware of. Though perhaps that is more of a modelling issue than a linguistic one.
I have no clue what does and does not work well with LLMs -- I'm just talking about explicit symbolic representation and (computer assisted/mechanised) reasoning; GOFAI but from a program logic perspective. Are you claiming that separation logic is unusable by LLMs? Or that it isn't helpful for capturing some essential aspects of framing in real-world problems?
This was a big concern when I was an undergrad in the 1990s. I've since wondered if bunched implications / separation logic / separation algebras / ... [1] that emerged in the early 2000s has resolved this well enough. Opinions?
At least some of the problem was due to people unnecessarily restricting themselves to first-order logic for knowledge representation, as advocated by John McCarthy [2].
I had a look at George Stiny's "Shape: Talking about Seeing and Doing" book (MIT Press, 2006) which is freely available on the web [1]. The introduction is very waffly ... his analysis of shape strikes me as what Euclid('s predecessors) did a long time ago in figuring out what geometry should talk about. Combining primitive images/shapes algebraically was explored by Henderson in the early 1980s [2] and many others; SICP too IIRC.
Has anyone used this stuff (shape grammars) in anger? Any pointers to a system that works on current platforms that is worth playing with?
There's a tonne of work done in this space, e.g. Mary Sheeran's µFP from the early 1980s [1], at least for classical synchronous digital circuits. Some googling will dig up a survey or two on modelling circuits with functions and a variety of systems in various languages. BlueSpec was and perhaps is interesting too but is quite a different approach.
> We can't prove that the axioms of arithmetic are consistent [...]
Sure we can! [1] ... but it requires (logically) stronger axioms. Assessing the relative strength of axioms along these (Gentzen's) lines goes by the name "ordinal analysis". It's not clear to me that stronger axioms are always less plausible than weaker ones (as axioms).
An alternative is to abandon your insistence on consistency. Another thread points to an article by Graham Priest but not to one of his main research interests: paraconsistency. This line of work aims to route around these issues (paradox in general) by making inconsistencies less explosive. A quick google turned up some relevant discussion [2]. I have it on good authority that the wheels fall off at some point.
For those looking for a broader/more portable introduction, Xavier Leroy and Didier Rémy wrote a great high-level text on UNIX system programming a long time ago [1]. Of course it uses ocaml (perhaps motivating some to learn that language) but the style is low-level and straightforwardly imperative. The advantage is that it sweeps up a lot of the messy and boring error handling into the ocaml runtime and/or exceptions. This makes the code a lot easier to follow, but of course makes it look misleadingly simpler than it would be in C (etc).
There were plans to build a hydrogen plant near Whyalla in South Australia, a famous steel-making site; see e.g. [1]. The tl;dr uses were export (I expected ammonia but the whole thing was vague enough to include hydrogen) on boats, reduction of iron ore ("decarbonisation", apparently requires magnetite) and while all the financial engineering that didn't happen was going to happen, energy storage for the grid, soaking up S.A.'s over-abundant solar.
Someone observed that this was the entirety of the presently-outgoing (but sure to be re-elected) state regime's story about reducing electricity bills in the state.
Thanks for the link! Some very pretty stuff there.
Missing AFAICT are categorical string diagrams. I'm only sort-of familiar with the notation for Haskell Arrows [1,2] but a quick google for "lambda calculus string diagrams" turns up some recent work by Dan Ghica and others that may be of interest.
If we're going down that path: Ehud Shapiro got there back in 1984 [1]. His PhD thesis is excellent and shows what logic programming could do (/could have been).
He viewed the task of learning predicates (programs/relations) as a debugging task. The magic is in a refinement operator that enumerates new programs. The diagnostic part was wildly insightful -- he showed how to operationalise Popper's notion of falsification. There are plenty of more modern accounts of that aspect but sadly the learning part was broadly neglected.
There are more recent probabilistic accounts of this approach to learning from the 1990s.
... and if you want to go all the way back you can dig up Gordon Plotkin's PhD thesis on antiunification from the early 1970s.
At the risk of telling you what you already know and/or did not mean to say: not everything can be a value. If everything is a value then no computation (reduction) is possible. Why? Because computation stops at values. This is traditional programming language/lambda calculus nomenclature and dogma. See Plotkin's classic work on PCF (~ 1975) for instance; Winskel's semantics text (~ 1990) is more approachable.
Things of course become a lot more fun with concurrency.
Now if you want a language where all the data thingies are immutable values and effects are somewhat tamed but types aren't too fancy etc. try looking at Milner's classic Standard ML (late 1970s, effectively frozen in 1997). It has all you dream of and more.
In any case keep having fun and don't get too bogged in syntax.
Hi Simurgh! This seems like a very ambitious project. I wonder if you've had a look at what others have done in this space. I initially liked the look of Ehud Shapiro's stuff [1] but I'm not sure he has the right take on the French political philosophy he draws on (or perhaps things have moved on now from the sources he cited). But perhaps his protocols are neutral enough to serve your purposes too?
The author is right to note that Haskell can optimise across module (abstraction) boundaries. However I remember that in my childhood that Debray [1] did a lot of work on link-time optimisations (late 1980s). And of course there's the classic self work that fed into the JVM [2], and the whole-of-program compilers that are receiving renewed attention now; mlton [3] being a classic of the genre, "supercompiler" being the active area of research AIUI. So at least sometimes abstraction boundaries are transparent to optimisers.
On the other hand the classic data abstraction story (signatures/interfaces for structures/modules) naturally allows for selecting or optimising implementations depending on uses. There was some great work done in the early 2000s on that (see [4]) and I'm sure the state-of-the-art has moved on since [5].
Yes, AIUI Streicher's work was in the vein of your [4]. (I got a vague pointer to him a while back; I don't know who's responsible for the meat of the development.)
Game semantics is expressive but AFAIK it has not (yet) provided new tools for reasoning about programs. I wonder why those tools have (apparently) not been developed, or do they just add (not very useful?) information to the old LCF story ala Scott? Has its moment passed?
By parallelism I think you mean concurrency. (Scott's domains have a bit too much parallelism as shown by Plotkin in his classic paper on LCF; these are at the root of the failure of Scott's models to be fully abstract.) And Scott's big idea -- that computation aligns with his notion of continuity -- conflicts with fairness which is essential for showing liveness. For this reason I never saw the point in powerdomains, excepting the Hoare (safety) powerdomain.
As these notes show, models, even adequate models, are a dime a dozen. It's formulating adequate reasoning principles that is tough. And that's what Andy Pitts brought to classic domain theory in the 1990s.
[0] https://en.wikipedia.org/wiki/Arrow_(computer_science)