The original point of Principia Mathematica's "theory of types" was to escape from Russell's Paradox. Russell's Paradox can be viewed as the problem of interpreting the statement, "This statement is false." A system of statements that permit such "paradoxes" is reducible to a directed cyclic graph of NOR (or NAND) gates -- generative logic, beyond first order logic -- that produces TIME (e.g. automata/computation). This should ring all kinds of bells with you, Ben. What Russell realized toward the end of his life was that just as dynamical systems in physics cannot be formally represented in closed form without imaginary arithmetic, so logic systems applicable to the real world (where time is essential) cannot be formally represented without imaginary logic "states" such as x = NOT(x). von Neumann actually tried to deal with this in his "quantum logic" at the dawn of the computer age, but failed where Tom Etter, in the 1990s, succeeded. Tom introduced the notion of negative case counts which, via particular symmetries corresponding to spinors, provide imaginary logic thence complex probability amplitudes implied by a relational structure. In this relational structure, physical dimensions, and their arithmetic, are an _inescapable_ consequence of what might be thought of as a programming language for quantum computers. See "2.4 Quantum Computers". <https://web.archive.org/web/20130511044913/http://www.boundaryinstitute.org/bi/articles/Link_Theory_intro.pdf>
In other words, trying to represent physical dimensions in the theory of types is getting the cart before the horse. You have to go back to the foundation of logic and build up from there to discover that computation is a dynamical system involving imaginary logic, and that "typing" is merely checking that two "objects" have commensurable dimensions (ie: they possess matching relational substructures required by a given operator). On Sun, Jul 5, 2020 at 10:16 AM Ben Goertzel <b...@goertzel.org> wrote: > I don't understand how the complaint about type theory connects w the > point about dimensions being ignored? > > E.g. in our thinking regarding revising/upgrading OpenCog we have been > looking at gradual typing, in which there can be multiple type systems > present in the same Atomspace metagraph, with decisions on what > type-system a given Atom is typed within made on a lazy basis... > > The importance of a "type system" as opposed to just a "set of > predicates labeling Atoms" is merely that a "type system" is expected > to come with an efficient type-checker which is a useful thing ... > (and not trivial if you are into dependent probabilistic types etc. > etc.) > > However it's certainly easy to implement physical dimensions at a > basic level in one's type system if one wants to > > The issue you raise doesn't seem to be about type theory as a > foundation for aspects of programming language design, but rather > about the choice of emphasis made by language developers in terms of > how they set up the specific set of types used in their languages... > > The point of type theory in language design is that, without efficient > type-checkers for specific type-systems, one would be stuck validating > program correctness using general purpose theorem proving which is > either very slow or AGI-hard... > > ben > > > > > On Sat, Jul 4, 2020 at 5:12 PM James Bowery <jabow...@gmail.com> wrote: > > > > I'm motivated to write this because, while doing a routine calculation > using an old 25 year old tool that no one ever much liked but a few people, > for whom I have the deepest respect, I found that it had been ported to > Javascript and is now online at http://www.calchemy.com/uclive.htm > > > > Here's what happened: > > > > I needed to calculate how much air flow my algae photobioreactor needed > to sustain growth of 32grams/meter^2/day extracting CO2 from air. Here's > what I entered. Try it: > > > > (6ft)^2*pi;32g > algae/m^2/day;416ppm(co2/air)*1.98kg/m^3;.505carbon/algae;.27 carbon/co2?L > air/sec > > > > I decided I need to go ahead and call the AirGas folks and tell them to > go ahead and deliver a CO2 dewar. > > > > The ';' operator says, "figure out the formula by dimensional > analysis". You can tell if the answer is sensible (and it does give you > the interpretation without the ';' as well as telling you if you have a > dimensional mismatch and what that mismatch might be). > > > > Open source now, too! Imagine a spreadsheet where a column "format" can > be units, and all you need to specify are the input columns to that column, > and the formula is derived by dimensional analysis. This can be done. > > > > "OK, cute stuff," you say. "Maybe even a big productivity booster for > hobbyists like you," you say, "but what's the big deal? I mean, C'mon... > 'Formal Language Theory Has Its Head Up Its Ass"? > > > > Yeah, I'm afraid so. I'll not bother writing again what I wrote as a > response over at "Alarming Development", but I will post it here again, > because it pretty much sums up not only how bad things are. > > > > James Bowery > > MARCH 12, 2019 AT 3:12 PM > > Feynman said that every physicist should have a sign with the number > “137” hanging on their door to remind them of how little the physics > community really knew — to keep them humble. To physicists, 137 is an > embarrassment that they all know about but, like the crazy aunt in the > attic, no one wants to talk about. > > > > There is a similar humbling and embarrassing aphorism that all computer > language designers should hang on their doors: > > > > “Miles and Kilometers are not data types and Distance is not an abstract > data type.” > > > > Whenever I run across “type theory” as the theoretic foundation for > programming languages (meaning all the time), I bristle. Bertrand Russell > said his theory of types was “…not really a theory but a stopgap.” “Type > theory”, as the basis for formal verification, has built an impressive > edifice on this bad foundation. Type theories, and resulting programming > language design, seem a kind of cargo cult, ritualistically pursued by > later minds. > > > > My question to programming language designers is simply this: > > > > Why the elaborate “type theories” while empirical dimensions of the real > world are ignored in formal foundations to the point that we have billion > dollar investments in space probes going to waste because someone failed to > do the appropriate conversion from miles to kilometers? > > > > After a 40 year career as a programmer dealing with life and death > issues in nuclear reactors and automated ordnance and aerospace inspection, > it is difficult to express my frustration. > > > > Adding “units” and “dimensions” as an afterthought to programming > languages evinces a deep philosophical problem not just in programming > languages, but in the foundations of mathematics. As Bertrand Russell said > of his now-long-forgotten “relation arithmetic”: > > > > “I think relation-arithmetic important, not only as an interesting > generalization, but because it supplies a symbolic technique required for > dealing with structure. It has seemed to me that those who are not familiar > with mathematical logic find great difficulty in understanding what is > meant by ‘structure’, and, owing to this difficulty, are apt to go astray > in attempting to understand the empirical world. For this reason, if for no > other, I am sorry that the theory of relation-arithmetic has been largely > unnoticed.” > > > > Although I was able to provide some support in revival of Relation > Arithmetic while at HP’s “Internet Chapter II” project, that effort was > quickly killed. > > > > > https://web.archive.org/web/20130806070425/http://www.boundaryinstitute.org/bi/articles/Relation-arithmetic_Revived_v3.pdf > > > > The $500M funding for “Internet Chapter 2” was urgently required to > import more H-1bs. And, no, that’s not just a bitter old man talking — I > was specifically ordered not to hire Tom Etter, whose mathematical > background was critical to the effort to bring relational dimensions we are > all familiar with into the foundations of mathematics thence programming > languages, and to hire instead H-1b workers. There is something going on > here that won’t stand the light of day and no one dares talk about it for > reasons that are now glaringly obvious. > > > > https://youtu.be/JQCJCTgzCFo?t=756 > > > > > > > > > > Artificial General Intelligence List / AGI / see discussions + > participants + delivery options Permalink > > -- > Ben Goertzel, PhD > http://goertzel.org > > “The only people for me are the mad ones, the ones who are mad to > live, mad to talk, mad to be saved, desirous of everything at the same > time, the ones who never yawn or say a commonplace thing, but burn, > burn, burn like fabulous yellow roman candles exploding like spiders > across the stars.” -- Jack Kerouac ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/T044a258b4a99cfd7-M02e676529db1c13500ca7acd Delivery options: https://agi.topicbox.com/groups/agi/subscription
