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