discarded1023

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.

Thanks for the reply and pointers.

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].

[1] https://en.wikipedia.org/wiki/Separation_logic

[2] see e.g. https://www-formal.stanford.edu/jmc/concepts.pdf

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?

[1] https://web.archive.org/web/20140105105101/http://shapetalki...

[2] https://dl.acm.org/doi/pdf/10.1145/800068.802148

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.

[1] see e.g. https://www.jucs.org/jucs_11_7/hardware_design_and_functiona...

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.

[1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof

[2] https://math.stackexchange.com/questions/1524715/how-do-inco...

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).

[1] https://ocaml.github.io/ocamlunix/

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.

[1] https://research.csiro.au/hyresource/south-australian-govern...

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.

[1] https://en.wikipedia.org/wiki/String_diagram

[2] Ross Paterson "A New Notation for Arrows" (2001)

Here's another from a long time ago: https://dkeenan.com/Lambda/

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.

[1] https://en.wikipedia.org/wiki/Algorithmic_program_debugging

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.

Where do Hughes's Arrows fit in?

You'd like to know your fault tolerance is reliable and possibly even correct.

A fantastic long read on this issue from a Glaswegian perspective (2022): https://www.lrb.co.uk/the-paper/v44/n18/ian-jack/chasing-ste...

Luca Cardelli worked on this stuff a while back [1]. Perhaps "systems biology" [2] might provide an entry to the literature.

[1] https://en.wikipedia.org/wiki/Luca_Cardelli

[2] https://en.wikipedia.org/wiki/Systems_biology

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?

[1] https://www.weizmann.ac.il/math/shapiro/home

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].

[1] https://dblp.org/pid/d/SKDebray.html

[2] https://en.wikipedia.org/wiki/Self_(programming_language)

[3] http://mlton.org/

[4] https://dblp.org/pid/59/4501.html

[5] https://en.wikipedia.org/wiki/Interprocedural_optimization

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.

Fantastic news and well deserved; even when Andy Pitts goes categorical his papers are very readable.

I got told a while ago that Streicher's "sequential" domains had solved the full abstraction problem for PCF [1] ... was it that or something else that killed off the work on game semantics?

It seems that Jon Sterling, author of the tool used to express the thoughts at the link, has made recent progress in domain theory [2] but perhaps the "synthetic" qualifier means it's not the real thing?

[1] Streicher's notes/book on domain theory sketches the construction but does not take it anywhere; I wonder what the reasoning principles are.

[2] see e.g. https://www.jonmsterling.com/jms-0064/index.xml

Thanks for the link. Is there anything new in these notes? They are cleanly presented but look like the greatest hits up to about 1982. Is there anything in there about reasoning about domains? e.g. what Andy Pitts made hay out of in the 1990s.

Yes, I was unaware of Smolka's early work and it does look very nice. (Much of Smolka's work seems underappreciated.) The evaluation in the paper under discussion of this work seems weak given that Smolka's early effort has a very similar set of features to what they want.

I concur about the research silo-ing. However in this case we have Europeans ignoring Europeans, and on that CTM page you will find a grab from a review in the Journal of Functional Programming. Several authors of this paper have published in the JFP, leading me to conclude that the JFP is a write-only journal, like much of CS literature.

I can't speak to the point of doing this, but (IIRC/IIUC) you're talking paths and they're talking the entire computation tree, i.e., a term in their calculus represents all solutions, and computing normal forms makes them easy to read off (?). Perhaps there's some meat in how they handle the equivalent of `bagof/3`/`setof/3`.

It's a nice write up but I'm not sure what the contribution is. I would have expected more engagement with Peter Van Roy's work, in particular his and Seif Haridi's epic book CTM [1] where the logic variable got properly unpacked more than 15 years previously. Or at least a citation.

Has anyone looked into how to decouple logic variables from backtracking? i.e., is there a good reason to unbind a variable apart from the Prolog discipline? (Without unbinding we get single-assignment variables where initialisation is decoupled from declaration, which I feel can often be simulated with laziness ala Haskell, but see CTM.)

[1] https://webperso.info.ucl.ac.be/~pvr/book.html

@JoeDaDude -- on macOS using recent Chrome/FireFox the puzzles linked from the top-level page yield terminal JavaScript errors. It'd be great to see them in action.

http://logicmazes.com/alice.html

  alice.html:353 Uncaught TypeError: Cannot read properties of undefined (reading 'play')
      at playSound (alice.html:353:30)
      at finalize2 (alice.html:347:1)
      at <anonymous>:1:1

Perhaps "Six Sources of Collapse" [1] may be what you're looking for.

[1] https://en.wikipedia.org/wiki/Charles_Robert_Hadlock

Enjoy it mate, and all the other fat Brunners. (His Stand on Zanzibar is most of Gibson's Neuromancer ... more than a decade before.) Give the thin ones a miss.

On a related note, for those who don't mind reading 17k words on industrial decline, is Ian Jack's great take on (civilian) shipbuilding in Glasgow.

The relevance to TFA is the difficulty of recovering the arts of ship construction lost to offshoring, financial engineering, politics, whatever. And it's a great read.

[1] https://www.lrb.co.uk/the-paper/v44/n18/ian-jack/chasing-ste...

I wonder how this relates to the old combinator-based approaches of Peter Henderson [1] and the logic-programming version [2]. Guy Cousineau also had a go with "Functional programming and geometry" in the late 1990s. I guess we'd say these are capable of describing corecursive pictures now.

I always felt this stuff would make a better foundation for web layouts than CSS.

[1] https://dl.acm.org/doi/pdf/10.1145/800068.802148

[2] Logic programming, graphics and infinite terms P. R. Eggert, K. P. Chow Department of Computer Science University of California, Santa Barbara UCSB DoCS TR 83-02 June 1983.

The author, Larry Paulson, may or may not like ZF but he has a ton of experience in doing formal proofs in it.

https://isabelle.in.tum.de/website-Isabelle2020/dist/library...