Linas, 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.
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. 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. - Ivan V. - 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.
