discarded1023
Joined 6 years ago
Karma
119
Submissions
52
Member since
Sep 21
Recent submissions
Comment · 2 months ago
Comment · 2 months ago
The game theorists/economists have studied this stuff in depth under the rubric of "mechanism design" or "market design". The relevant concept is "incentive compatibility" where the agents in the system do the right thing (whatever that was intended to be/designed for) because any deviation from that costs them more than playing nice.
The Wikipedia article [0] is not yet great but does give the two classic examples of "second-price auctions and a simple majority vote between two choices". The Gibbard–Satterthwaite shows the difficulty in extending this to more choices (in that Arrow's theorem sort of way).
The best thing I've read on this stuff is Alvin Roth's "Who Gets What and Why" (2015) [1] which is worth a read in any case. Repugnant markets!
[0] https://en.wikipedia.org/wiki/Incentive_compatibility
[1] https://en.wikipedia.org/wiki/Alvin_E._Roth#Market_design
Comment · 3 months ago
> Similarly when people say "the rationals are countable" and "the computable numbers are countable" this is taking for granted the Cantor notion of measuring cardinality by bijective correspondence, once again, a theory that yields nothing of value except endless paradoxes and naval-gazing nonsense.
You may enjoy a recent update on that story [0] that maybe avoids a few paradoxes and looks at things other than navels.
Comment · 3 months ago
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.
Comment · 5 months ago
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.
Comment · 5 months ago
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?
Comment · 5 months ago
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
Comment · 6 months ago
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...
Comment · 6 months ago
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...
Comment · 7 months ago
> 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...
Comment · 7 months ago
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).
Comment · 7 months ago
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...
Comment · 8 months ago
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)
Comment · 8 months ago
Here's another from a long time ago: https://dkeenan.com/Lambda/
Comment · 8 months ago
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
[0] https://theconversation.com/three-things-australia-must-do-t...