On Tue, Dec 11, 2018 at 2:24 AM Ivan Vodišek <[email protected]> wrote:
> Thank you for taking a time to response, I'll try to keep this short. I might > be wrong, but Curry-Howard-Lambek isomorphism inspires me greatly in a > pursuit for one-declarative-language-like-URE-to-rule-them-all. One silly remark, and one serious remark; silly one first: Curry-Howard correspondence extends all the way to tensor algebras, quantum mechanics, string theory and cobordisms. If you have the time and the willpower, John Baez "Rosetta Stone" is a simple, straightforward introduction. Curry-Howard also plays a big/central role in type theory, see "the HoTT book". The first few chapters of that provide a nice readable introduction to type theory. (and requires much less background than Baez) Re: URE: So curry-howard says "proofs are programs" and it turns out that theorem proving is a lot like parsing (its identical to parsing???) I DO NOT know of any simple write-up of this topic; I can only wave my hands around. When I mentioned this to Ben's son Zar, he kind-of responded and said "duhh its obvious everyone knows this." Zar, do you know of any nice readable references that explain how theorem-proving and parsing are "the same thing"? Anyway, there is more than one way of combining rules to obtain proofs. URE uses forward/backward chaining. It is "well known" that SAT-solving is orders of magnitude faster than forward-backward chaining. As to parsing, I've been hacking on link-grammar. Amir now has it so that its as fast or faster than the SAT solver more or less. So URE is not the only way, it is "a way". And also .. openpsi is yet another alternative, but I'm not prepared to talk about that. > I see term rewriting simply as basic implication over input and output terms. > A number of term rewriting rules may be bundled together in a conjunction. > Alternate pattern-matching options may form a disjunction. And pattern > exclusion may be expressed as a negation. These are all common logical > operators in a role of defining a term rewriting system. And since this kind > of term rewriting is basically a logic, it can generally be tested for > contradiction, or it can be used for deriving relative indirect rules - if we > want it so. Sure. This is what the atomspace pattern-matcher does. It's effectively crisp logic. Its also got a rich selection of bells and whistles; for example, user-defined callbacks in various places, to alter what it does: reorder, rank, select-top-N, search-this-first. Support for virtual terms: `if x<y` . Support for term-absence: `if (a found but b absent)` etc. Its gotten big, hard to understand as a result. A bit crufty in places, but we've kept it mostly clean and pretty fast. But again: when you say "Alternate pattern-matching options may form a disjunction." etc. well -- hey, this is exactly what link-grammar does. You can read the link-grammar dicts, and explicitly see conjunctions and disjunctions. <noun-main-x>: (S+ & <CLAUSE>) or SI- or J- or O- or <post-nominal-x> or <costly-null>; This is very similar to what the opencog pattern matcher works with, but uses a very different notation, and a very different "shallow theory". But in a deep sense, the two are the same, and I'm trying to work my way so that the code, the API's, the implementation provide a more unified, more cohesive view of both. So that the URE can eventually become a parser, instead of a chainer. (or offer a parser component, in addition to a chainer component). So what you are doing is all good. With these emails, I'm trying to point out "what we've learned so far". > That's a short version of what I currently work on - a term rewriting system > expressed as a crisp logic - just a few basic logic operators with no > hard-wired constants other than true and false - all wrapped up in a human > friendly code code processor. Yes, this seems reasonable. I forget, what language are you working in? is this in git somewhere? -- Linas > uto, 11. pro 2018. u 04:07 Linas Vepstas <[email protected]> napisao je: >> >> On Sun, Dec 9, 2018 at 11:55 AM Ivan Vodišek <[email protected]> wrote: >> > >> > Oh, I see, I must be talking about URE then. All cool, then it seems >> > reasonable to me (one ring to rule them all - policy). >> > >> > I keep persuading myself that a perfect single declarative - logic + >> > lambda calculus + type theory exists, or could be invented, >> >> So, OK, the atomspace is trying to be: >> >> + declarative: so kind-of-like datalog or kind-of like SQL or noSQL, >> or some quasi-generic (graph) data store. But you already know this. >> >> - it does NOT have "logic" in it, in any traditional sense of the word >> "logic". It does have the ability to perform term-rewriting (pattern >> re-writing, graph re-writing). >> >> - lambda calculus is a form of "string rewriting". Note that string >> rewriting is closely related to term rewriting (but not quite the same >> thing) and that term rewriting is closely related to graph rewriting >> (but not quite the same thing). >> >> When lambda calculus was invented, any distinction between strings, >> terms, and graphs was unknown and unknowable, until the basic concepts >> got worked out. So, due to "historical accident", generic lambda >> calculus remains a string rewriting system. As stuff got worked out >> over the 20th century, the concept of "term rewriting" gelled as a >> distinct concept. (And other mind-bendingly >> similar-but-slightly-different ideas, like universal algebra, model >> theory ... and bite my tongue. There's more that's "almost the same as >> lambda calc. but not quite". A veritable ocean of closely related >> ideas.) >> >> From practical experience with atomspace, it turns out that trying to >> pretend that all three rewriting styles (string, term, graph) are the >> same thing "mostly works", but causes all kinds of friction, >> confusion, conundrums in detailed little corners. So, for example, >> BindLink was an early attempt to define a Lambda for declarative >> graphs. In many/most ways, it really is "just plain-old-lambda". It >> works, and works great to this day, but, never-the-less, we also >> created more stuff that is "just like lambda, but different", >> including LambdaLink, etc. >> >> In many ways, its an ongoing experiment. The search for "perfect" has >> more recently lead to "values", which are a lot like "valuations" in >> model theory. (and again, recall that model-theory is kind-of-ish like >> lambda-calculus, but its typed.) >> >> There's no "logic" in the atomspace, but you could add logic by using >> the URE, and/or by several other ways, including parsing, sheaves, and >> openpsi. In short, there's lots of different kinds of logic, and lots >> of different ways of implementing it, and we are weakly fiddling with >> several different approaches. And I have more in mind, but lacking in >> time. >> >> -- Linas >> -- >> cassette tapes - analog TV - film cameras - you >> >> -- >> 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/CAHrUA35V2Uk0YbwERPMkPhpxevriT0DZvaYzLtEPXUQC9TiUHQ%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/CAB5%3Dj6VaDej%3DGBL3bpMxYArP6ZnkifCiNmStc7-SrJO%2BV3eHQA%40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. -- cassette tapes - analog TV - film cameras - you -- 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/CAHrUA35oEJMyqNGSvM_QjYWTTRj%3D_MMQFT3y7%3D7fg%3D-rEzQ-TQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
