Hi Ben, OK, not sure what to say. I think you totally missed the point of my last email. Specifically, it is a https://en.wikipedia.org/wiki/Category_mistake which is a punny way of putting it.
So let me try again a different way: you are a big fan of agda -- so -- a rhetorical question: which logic is agda based on? https://en.wikipedia.org/wiki/Type_theory "Some other type theories include Per Martin-Löf's intuitionistic type theory, which has been the foundation used in some areas of constructive mathematics and for the proof assistant Agda. Thierry Coquand's calculus of constructions and its derivatives are the foundation used by Coq and others. The field is an area of active research, as demonstrated by homotopy type theory." "Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like Idris, ATS, Agda and Epigram." "A prime example is Agda, a programming language which uses intuitionistic type theory for its type system." "intuitionistic type theory is used by Agda which is both a programming language and proof assistant; https://en.wikipedia.org/wiki/Intuitionistic_logic "As such, the use of proof assistants (such as Agda or Coq) is enabling modern mathematicians and logicians to develop and prove extremely complex systems,..." https://en.wikipedia.org/wiki/Intuitionistic_type_theory "Type theory has been the base of a number of proof assistants, such as NuPRL, LEGO and Coq. Recently, dependent types also featured in the design of programming languages such as ATS, Cayenne, Epigram, Agda, and Idris." https://ncatlab.org/nlab/show/Agda "Besides Coq, Agda is one of the languages in which homotopy type theory has been implementsed" https://books.google.com/books?id=Wz2qCAAAQBAJ&pg=PA240&lpg=PA240&source=bl&ots=9iiojQwhMg&sig=2XzQEZXuAv8QIgvyBcj0T6gk4pM&hl=en&sa=X&ved=0ahUKEwjvy8LKpuzOAhUM5WMKHd50AakQ6AEIUjAI#v=onepage well -- I can't cut-n-paste -- its a copyright-protected e-book. ------------- The category mistake is this: do NOT confuse the DOMAIN, with REASONING ABOUT THE DOMAIN. Which is what is being done, when you start talking about PLN. I am NOT talking about PLN. I am talking about REASONING ABOUT PLN! Two different things. I mentioned "ludics" for a reason. Think of it this way: you can write any program at all in agda. For example, it could be a program that adds two integers together, and prints the result. So, agda uses intuitionistic logic to *run* that program. That does not mean the addition of integers needs, uses, requires intuitionistic logic. It only means that, if you write your program in agda, that is the theory of logic that will be used to run your program. Think of PLN as being the program that adds integers together. Or however you want to describe what PLN does. It is what it is. I am trying to talk about the correct way in which to implement the *algorithm* that implements PLN. Until we get past this point, we will be confused about what we are talking about. Same deal for relex2logic. Same deal for relex. Same deal for linkages in link-grammar. Same deal for the so-called "word-graph" tokenizer that Amir implemented for link-grammar, to split up words into morphemes. Ask Amir to explain how it works. You promptly get kripke frames, and NOT classical logic! --linas On Tue, Aug 30, 2016 at 5:10 PM, Ben Goertzel <[email protected]> wrote: > Linas, > > Actually, even after more thought, I still don't (yet) see why linear > logic is needed here... > > In PLN, each statement is associated with at least two numbers > > (strength, count) > > Let's consider for now the case where the strength is just a probability... > > Then in the guilt/innocence case, if you have no evidence about the > guilt or innocence, you have count =0 .... So you don't have to > represent ignorance as p=.6 ... you can represent it as > > (p,n) = (*,0) > > The count is the number of observations made to arrive at the strength > figure... > > PLN count rules propagate counts from premises to conclusions, and if > everything is done right without double-counting of evidence, then the > amount of evidence (number of observations) supporting the conclusion > is less than or equal to the amount of evidence supporting the > premises... > > This does not handle estimation of resource utilization in inference, > but it does handle the guilt/innocence example > > As for the resource utilization issue, certainly one can count the > amount of space and time resources used in drawing a certain inference > ... and one can weight an inference chain via the amount of resources > it uses... and one can prioritize less expensive inferences in doing > inference control. This will result in inferences that are "simpler" > in the sense of resource utilization, and hence more plausible > according to some variant of Occam's Razor... > > But this is layering resource-awareness on top of the logic, and using > it in the control aspect, rather than sticking it into the logic as > linear and affine logic do... > > The textbook linear logic example of > > "I have $5" ==> I can buy a sandwich > "I have $5" ==> I can buy a salad > |- (oops?) > "I have $5" ==> I can buy a sandwich and I can buy a salad > > doesn't impress much much, I mean you should just say > > If I have $5, I can exchange $5 for a sandwich > If I have $5, I can exchange $5 for a salad > After I exchange $X for something else, I don't have $X anymore > > or whatever, and that expresses the structure of the situation more > nicely than putting the nature of exchange into the logical deduction > apparatus.... There is no need to complicate one's logic just to > salvage a crappy representational choice... > > In linear logic: It is no longer the case that given A implies B and > given A, one can deduce both A and B ... > > In PLN, if one has > > A <sA, nA> > (ImplicationLink A B) <sAB, nAB> > > one can deduce > > B <sB,nB> > > but there is some math to do to deduce sB and nB, and one can base > this math on various assumptions including independence assumptions, > assumptions about the shapes of concepts, etc. > > In short I think if we extent probabilistic TTR to be "TTR with <p,n> > truth values", then we can use lambda calculus with a type system > drawn from TTR and with each statement labeled with a <p,n> truth > value ... and then we can handle the finitude of evidence without > needing to complicate the base logic... > > A coherent and sensible way to assess <p,n> truth values for > statements with quantified variables was given by me and Matt in 2008, > in > > http://www.agiri.org/IndefiniteProbabilities.pdf > > Don't let the third-order probabilities worry you ;) > > ... > > In essence, it seems, the linear logic folks push a bunch of > complexity into the logic itself, whereas Matt and I pushed the > complexity into the truth values, and the Occam bias on proofs (into > which resource utilization should be factored) > > -- Ben > . > > > > On Tue, Aug 30, 2016 at 6:52 PM, Linas Vepstas <[email protected]> > wrote: > > Hi Ben, > > > > Well, it might not have to be linear, it might be affine, I have not > thought > > it through myself. What is clear is that cartesian is clearly wrong. > > > > The reason I keep repeating the guilt/innocence example is that its not > just > > the "exclusive nature of disjuncts in link-grammar", but rather, that it > is > > a generic real-world reasoning problem. > > > > I think I understand one of the points of confusion, though. In digital > > circuit verification (semiconductor chip industry), everyone agrees that > the > > chips themselves behave according to classical boolean logic - its all > just > > ones and zeros. However, in verification, you have to prove that a > > particular chip design is working correctly. That proof process does NOT > > use classical logic to achieve its ends -- it does use linear logic! > > Specifically, the proof process goes through sequences of Kripke frames, > > where you verify that certain ever-larger parts of the chip are behaving > > correctly, and you use the frames to keep track of how the various > > combinatorial possibilities feed back into one another. Visualize it as > a > > kind of lattice: at first, you have a combinatoric explosion, a kind of > tree > > or vine, but then later, the branches join back together again, into a > > smaller collection. Those that fail to join up are either incompletely > > modelled, or indicate a design error in the chip. > > > > There's another way of thinking of chip verification: one might say, in > any > > given universe/kripke frame, that a given transistor is in one of three > > states: on, off, or "don't know", with the "don't know" state > corresponding > > to the "we haven't simulated/verified that one yet". The collection of > > possible universes shrinks, as you eliminate the "don't know" states > during > > the proof process. This kind of tri-valued logic is called > > "intuitionistic logic" and has assorted close relationships to linear > logic. > > > > These same ideas should generalize to PLN: although PLN is itself a > > probabilistic logic, and I do not advocate changing that, the actual > > chaining process, the proof process of arriving at conclusions in PLN, > > cannot be, must not be. > > > > I hope the above pins down the source of confusion, when we talk about > these > > things. The logic happening at the proof level, the ludics level, is > very > > different from the structures representing real-world knowledge. > > > > --linas > > > > On Tue, Aug 30, 2016 at 9:28 AM, Ben Goertzel <[email protected]> wrote: > >> > >> Linas, > >> > >> Alas my window of opportunities for writing long emails on math-y > >> stuff has passed, so I'll reply to your email more thoroughly in a > >> couple days... > >> > >> However, let me just say that I am not so sure linear logic is what we > >> really want.... I understand that we want to take resource usage into > >> account in our reasoning generally... and that in link grammar we want > >> to account for the particular exclusive nature of the disjuncts ... > >> but I haven't yet convinced myself linear logic is necessarily the > >> right way to do this... I need to take a few hours and reflect on it > >> more and try to assuage my doubts on this (or not) > >> > >> -- ben > >> > >> > >> On Tue, Aug 30, 2016 at 6:14 AM, Linas Vepstas <[email protected]> > >> wrote: > >> > It will take me a while to digest this fully, but one error/confusion > >> > (and > >> > very important point) pops up immediately: link-grammar is NOT > >> > cartesian, > >> > and we most definitely do not want cartesian-ness in the system. That > >> > would > >> > destroy everything interesting, everything that we want to have. > Here's > >> > the > >> > deal: > >> > > >> > When we parse in link-grammar, we create multiple parses. Each parse > >> > can be > >> > considered to "live" in its own unique world or universe (it's own > >> > Kripke > >> > frame) These universes are typically incompatible with each other: > they > >> > conflict. Only one parse is right, the others are wrong (typically -- > >> > although sometimes there are some ambiguous cases, where more than one > >> > parse > >> > may be right, or where one parse might be 'more right' than another). > >> > > >> > These multiple incompatible universes are symptomatic of a "linear > type > >> > system". Now, linear type theory finds applications in several > places: > >> > it > >> > can describe parallel computation (each universe is a parallel thread) > >> > and > >> > also mutex locks and synchronization, and also vending machines: for > one > >> > dollar you get a menu selection of items to pick from -- the > ChoiceLink > >> > that > >> > drove Eddie nuts. > >> > > >> > The linear type system is the type system of Linear logic, which is > the > >> > internal language of the closed monoidal categories, of which the > closed > >> > cartesian categories are a special case. > >> > > >> > Let me return to multiple universes -- we also want this in PLN > >> > reasoning. A > >> > man is discovered standing over a dead body, a bloody sword in his > hand > >> > -- > >> > did he do the deed, or is he simply the first witness to stumble onto > >> > the > >> > scene? What is the evidence pro and con? > >> > This scenario describes two parallel universes: one in which he is > >> > guilty, > >> > and one in which he is not. It is the job of the prosecutor, defense, > >> > judge > >> > and jury to figure out which universe he belongs to. The mechanism > is a > >> > presentation of evidence and reasoning and deduction and inference. > >> > > >> > Please be hyper-aware of this, and don't get confused: just because we > >> > do > >> > not know his guilt does not mean he is "half-guilty", -- just like an > >> > unflipped coin is not a some blurry, vague superimposition of heads > and > >> > tails. > >> > > >> > Instead, as the evidence rolls in, we want to find that the > probability > >> > of > >> > one universe is increasing, while the probability of the other one is > >> > decreasing. Its just one guy -- he cannot be both guilty and innocent > >> > -- > >> > one universe must eventually be the right one,m and it can be the only > >> > one. > >> > (this is perhaps more clear in 3-way choices, or 4-way choices...) > >> > > >> > Anyway, the logic of these parallel universes is linear logic, and the > >> > type > >> > theory is linear type theory, and the category is closed monoidal. > >> > > >> > (Actually, I suspect that we might want to use affine logic, which is > >> > per > >> > wikipedia "a substructural logic whose proof theory rejects the > >> > structural > >> > rule of contraction. It can also be characterized as linear logic with > >> > weakening.") > >> > > >> > Anyway, another key point: lambda calculus is the internal language of > >> > *cartesian* closed categories. It is NOT compatible with linear logic > >> > or > >> > linear types. This is why I said in a different email, that "this > way > >> > lies > >> > madness". Pursuit of lambda calc will leave us up a creek without a > >> > paddle, > >> > it will prevent us from being able to apply PLN to guilty/not-guilty > >> > court > >> > cases. > >> > > >> > ---- > >> > BTW, vector spaces are NOT cartesian closed! They are the prime #1 > most > >> > common example of where one can have tensor-hom adjunction, i.e. can > do > >> > currying, and NOT be cartesian! Vector spaces *are* closed-monoidal. > >> > > >> > The fact that some people are able to map linguistics onto vector > spaces > >> > (although with assorted difficulties/pathologies) re-affirms that > >> > closed-monoidal is the way to go. The reason that linguistics maps > >> > poorly > >> > onto vector spaces is due to their symmetry -- the linguistics is NOT > >> > symmetric, the vector spaces are. So what we are actually doing (or > >> > need > >> > to do) is develop the infrastructure for *cough cough* a non-symmetric > >> > vector space.. which is kind-of-ish what the point of the categorial > >> > grammars is. > >> > > >> > Enough for now. > >> > > >> > --linas > >> > > >> > > >> > On Mon, Aug 29, 2016 at 4:41 PM, Ben Goertzel <[email protected]> > wrote: > >> >> > >> >> Linas, Nil, etc. -- > >> >> > >> >> This variation of type theory > >> >> > >> >> http://www.dcs.kcl.ac.uk/staff/lappin/papers/cdll_lilt15.pdf > >> >> > >> >> seems like it may be right for PLN and OpenCog ... basically, > >> >> dependent type theory with records (persistent memory) and > >> >> probabilities ... > >> >> > >> >> If we view PLN as having this sort of semantics, then RelEx+R2L is > >> >> viewed as enacting a morphism from: > >> >> > >> >> -- link grammar, which is apparently equivalent to pregroup grammar, > >> >> which is a nonsymmetric cartesian closed category > >> >> > >> >> to > >> >> > >> >> -- lambda calculus endowed with the probabilistic TTR type system, > >> >> which is a locally cartesian closed category > >> >> > >> >> > >> >> > >> >> https://ncatlab.org/nlab/show/relation+between+type+theory+ > and+category+theory#DependentTypeTheory > >> >> > >> >> For the value of dependent types in natural language semantics, see > >> >> e.g. > >> >> > >> >> > >> >> > >> >> http://www.slideshare.net/kaleidotheater/hakodate2015- > julyslide?qid=85e8a7fc-f073-4ded-a2c8-9622e89fd07d&v=&b=&from_search=1 > >> >> > >> >> (the examples regarding anaphora in the above are quite clear) > >> >> > >> >> > >> >> > >> >> https://ncatlab.org/nlab/show/dependent+type+theoretic+ > methods+in+natural+language+semantics > >> >> > >> >> This paper > >> >> > >> >> > >> >> > >> >> http://www.slideshare.net/DimitriosKartsaklis1/ > tensorbased-models-of-natural-language-semantics?qid= > fd4cc5b3-a548-46a7-b929-da8246e6c530&v=&b=&from_search=2 > >> >> > >> >> on the other hand, seems mathematically sound but conceptually wrong > >> >> in its linguistic interpretation. > >> >> > >> >> It constructs a nice morphism from pregroup grammars (closed > cartesian > >> >> categories) to categories defined over vector spaces -- where the > >> >> vector spaces are taken to represent co-occurence vectors and such, > >> >> indicating word semantics.... The morphism is nice... however, the > >> >> idea that semantics consists of numerical vectors is silly ... > >> >> semantics is much richer than that > >> >> > >> >> If we view grammar as link-grammar/pregroup-grammar/asymmetric-CCC > ... > >> >> we should view semantics as {probabilistic TTR / locally compact > >> >> closed CCC *plus* numerical-vectors/linear-algebra} > >> >> > >> >> I.e. semantics has a distributional aspect AND ALSO a more explicitly > >> >> logical aspect > >> >> > >> >> Trying to push all of semantics into distributional word vectors, > >> >> leads them into insane complexities like modeling determiners using > >> >> Frobenius algebras... which is IMO just not sensiblen ... it's trying > >> >> to achieve a certain sort of mathematical simplicity that does not > >> >> reflect the kind of simplicity seen in natural systems like natural > >> >> language... > >> >> > >> >> Instead I would say RelEx+R2L+ECAN (on language) + > >> >> word-frequency-analysis can be viewed as enacting a morphism from: > >> >> > >> >> -- link grammar, which is apparently equivalent to pregroup grammar, > >> >> which is a nonsymmetric cartesian closed category > >> >> > >> >> to the product of > >> >> > >> >> -- lambda calculus endowed with the probabilistic TTR type system, > >> >> which is a locally cartesian closed category > >> >> > >> >> -- the algebra of finite-dimensional vector spaces > >> >> > >> >> This approach accepts fundamental heterogeneity in semantic > >> >> representation... > >> >> > >> >> -- Ben > >> >> > >> >> -- > >> >> Ben Goertzel, PhD > >> >> http://goertzel.org > >> >> > >> >> Super-benevolent super-intelligence is the thought the Global Brain > is > >> >> currently struggling to form... > >> > > >> > > >> > -- > >> > You received this message because you are subscribed to the Google > >> > Groups > >> > "link-grammar" group. > >> > To unsubscribe from this group and stop receiving emails from it, send > >> > an > >> > email to [email protected]. > >> > To post to this group, send email to [email protected]. > >> > Visit this group at https://groups.google.com/group/link-grammar. > >> > For more options, visit https://groups.google.com/d/optout. > >> > >> > >> > >> -- > >> Ben Goertzel, PhD > >> http://goertzel.org > >> > >> Super-benevolent super-intelligence is the thought the Global Brain is > >> currently struggling to form... > >> > >> -- > >> You received this message because you are subscribed to the Google > Groups > >> "opencog" group. > >> To unsubscribe from this group and stop receiving emails from it, send > an > >> email to [email protected]. > >> To post to this group, send email to [email protected]. > >> Visit this group at https://groups.google.com/group/opencog. > >> To view this discussion on the web visit > >> https://groups.google.com/d/msgid/opencog/CACYTDBeRwpZiNS% > 3DShs2YfrRbKkC426v3z51oz6-Fc8u7SoJ8Mw%40mail.gmail.com. > >> For more options, visit https://groups.google.com/d/optout. > > > > > > -- > > You received this message because you are subscribed to the Google Groups > > "link-grammar" group. > > To unsubscribe from this group and stop receiving emails from it, send an > > email to [email protected]. > > To post to this group, send email to [email protected]. > > Visit this group at https://groups.google.com/group/link-grammar. > > For more options, visit https://groups.google.com/d/optout. > > > > -- > Ben Goertzel, PhD > http://goertzel.org > > Super-benevolent super-intelligence is the thought the Global Brain is > currently struggling to form... > > -- > You received this message because you are subscribed to the Google Groups > "opencog" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/opencog. > To view this discussion on the web visit https://groups.google.com/d/ > msgid/opencog/CACYTDBfYYLL1Lh_K1%2BYpfBLSpc_XK56HK38givQ5XC3cKxjMRg% > 40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "opencog" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/opencog. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAHrUA36GH_mpech8RPGxRa-EDq7atW12p4kODGQNWPYUQprTdQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
