All OpenCog mailng list members, I'm sorry I lost the temper, and roughly ended the conversation. It just happened that the conversation began to include more things than I was able to properly present, so things went a bit fuzzy for me.
You don't owe me anything, especially not to thoroughly study any nonsense I write as a guy watching from aside. So please, take my apology for being rude, especially to Linas, who is contributing a way better deal to this community than me. I'm sorry I abused your open minded attitude. - Ivan V. - čet, 13. pro 2018. u 12:55 Ivan Vodišek <[email protected]> napisao je: > Things got over-complicated in this thread. It became like you are trying > to explain some progressive math area to someone by having a > short-sequenced dialog. I think that this matter deserves a decent > monologue in a form of a "scientific" or at least "hand-waving" paper. > There are particular areas that should be read more slowly and carefully, > with understanding. With dialog, it is too easy to skim it fast and say > "impossible", "no", or "it's crazy" if something is not understood. I > believe I'd have a better chance with a proper monologue and a possible > question answering after that. The final goal would be a specific > proposition for improving OpenCog, instead of having an endless chitchat. > > - Ivan V. - > > > čet, 13. pro 2018. u 07:59 Linas Vepstas <[email protected]> napisao > je: > >> On Wed, Dec 12, 2018 at 2:28 AM Ivan Vodišek <[email protected]> >> wrote: >> > >> > I'm sorry, maybe I wasn't specific enough, what I just published is not >> a complete metalanguage (still have to do some real work for that). What in >> fact it represents is merely a CFG complete parsing algorithm, similar to >> GLR, CYK, Earley, LG... >> >> If by LG you mean "link-grammar", then thinking about it as if it were >> some 1960's context-free-grammar is asking for headaches. Yes, there >> might exist some algorithm to convert it into that. I've read (and >> lost the reference) a paper that made a hand-waving argument that >> algorithms always exist to convert dependency grammars into >> phrase-structure grammars. But it was hand-waving, and not a formal >> proof, and gave no hint at the required complexity. >> >> In general, don't assume that its easy or even desirable to convert >> other formats into 1960's style CFG's. >> >> > But this one is linear, as described. >> >> I'm pretty sure there are proofs that CFG's cannot, in general, be >> parsed in linear time. There's a stack, after all, and you can always >> make the stack grow arbitrarily deep. I don't think that even regular >> languages can be parsed in linear time. >> >> > So, why is this linearity important? You see, there exists Curry-Howard >> correspondence for a variety of systems. But I believe it extends even to >> parsers. To be specific, a parser could be represented by propositional >> calculus with extension of sequencing (something like predicates, but >> containing propositions instead of variables and functions). >> >> Don't know what you mean by "extended with sequencing". >> >> > >> > The following would be an example of a grammar defined in propositional >> logic with sequencing: >> > >> > ( >> > Sum -> ( >> > Sum "+" Mul \/ >> > Fact >> > ) >> > ) /\ ( >> > Fact -> ( >> > Fact "*" Primary \/ >> > Primary >> > ) >> > ) /\ ( >> > Primary -> /[0-9+]/ >> > ) /\ ( >> > TopSymbol -> Sum >> > ) >> >> That's hard to read. It looks like some production rules for >> generating sums and products of integers. Wouldn't BNF notation be >> easier? By not using BNF, are you trying to show something? >> >> Anyway, production rules are certainly not propositional calculus: >> TopSymbol cannot be reduced to true or false. TopSymbol could be >> reduced to a single integer. But production rules don't do that .. >> they only specify a language ... So I don't understand what you are >> trying to do here. >> >> > >> > Some contradictory grammar would represent a grammar that has no valid >> parsing example, i.e. always terminates with an error. Deriving a >> contradiction from such a grammar would include parsing each rule against a >> negation of every other rule, and if such a negation parsing succeeds, the >> current rule of focus is replaced by False. If any of such false parses >> apear directly below the root, the grammar is contradictory. If we now have >> a linear or even polynomial time complexity time parser algorithm, then P >> equals NP, under assumption that we replace parsing rules by any kind of >> logic propositions, while rule referencing is determined by the common >> resolution rule. Does this make sense? >> >> I don't understand any of this. What's a "contradictory grammar"? >> >> --linas >> >> > >> > I had other ideas for efficiently deriving contradiction too, but this >> approach seems relevant for this moment. >> > >> > Nevertheless, this is not enough for grounding symbols, in a same way >> that propositional logic is not expressive enough to describe some more >> complicated expressions. To make grounding possible, it is necessary to >> introduce some form of quantifying over variables, or even over the whole >> logic expressions in my case. I still have to finish this part, but it's on >> the schedule. >> > >> > - Ivan V. - >> > >> > >> > sri, 12. pro 2018. u 03:39 Linas Vepstas <[email protected]> >> napisao je: >> >> >> >> I'm not really clear on what it is that you are describing. Is it >> >> possible (even in principle) to take some typical atomese pattern and >> >> translate it into your notation? Can you represent something like >> >> "Ivan wrote some code. Linas took a shower. Ivan wrote $X" and run >> >> your system, and find that $X is grounded by "some code" ? What >> >> notation would you use to express this? Or are you describing >> >> something else? >> >> >> >> -- Linas >> >> >> >> >> >> >> >> >> >> On Tue, Dec 11, 2018 at 7:31 PM Ivan Vodišek <[email protected]> >> wrote: >> >> > >> >> > Hi Linas, >> >> > >> >> > I started to implement the language I'm talking about in Javascript >> some year ago. I finished a parser, put it on GitHub ( >> https://github.com/ivanvodisek/V-Parse), but got new ideas in a >> meanwhile for the language, including inspiration for a linear time SAT >> solver, which put me back to theoretical investigation. I really like what >> it looks like by now, as for both visual appearance and theoretical >> performance. >> >> > >> >> > The parser I implemented is actually based on a novel chart CFG >> algorithm that handles parsing trees in a certain way, which enables the >> parser to exhibit linear parsing time [yes, you read well, it is below >> O(n^3)], no matter of amount of ambiguity of resulting AST. In short, it is >> about organizing an AST in a chart sequence of parsed atoms (possibly >> branched on ambiguous match). The consequence of this organization is that >> at each offset we have at most |Grammar-complexity| amount of possible >> distinct atoms, and that takes [Grammar-complexity| amount of time (it is a >> constant time) to parse at each offset, hence linear time! This was a hard >> nut, but I think I made it. Not to stay just on words, you can test it by >> yourself on the above link, and my experimental readings align with >> theoretical linearity of the algorithm. The parser is not patented, nor >> will ever be (I don't believe in intellectual patents), and anyone is free >> to use it in whichever way he/she finds appropriate (I'd be actually >> honored if someone uses it for a good cause). If someone needs a help for >> porting it to C++ or Java, feel free to contact me, I'm pretty sure I can >> help. It probably needs certain tweaks to actually use it, but it should >> work if I'm not mistaken. >> >> > >> >> > I'm afraid I can't offer you more than this concrete result at the >> present time, but I'm working on it. Probably my next move is to try to >> implement linear time SAT solver also in Javascript, which will also be >> open licensed if it turns out it actually works (just theoretical analysis >> for now, hoping for experimental results soon). And the implementation of >> the language I'm dreaming about is pending after that. Wish me luck :-) >> >> > >> >> > - Ivan V. - >> >> > >> >> > "Dream big. The bigger the dream is, the more beautiful place the >> world becomes:" - me >> >> > >> >> > >> >> > sri, 12. pro 2018. u 01:17 Linas Vepstas <[email protected]> >> napisao je: >> >> >> >> >> >> Oh, and one more (minor?) remark: the intermediate states that get >> >> >> explored during pattern matching are called "Kripke frames", and the >> >> >> "crisp logic of term re-writing" is one of the modal logics. I know >> >> >> this to be true in a hand-waving fashion; I have searched long and >> >> >> hard for a paper or a book that would articulate this in some >> direct, >> >> >> detailed fashion. I have not yet found one. >> >> >> >> >> >> Zar, so second question, any chance at all you might be aware of >> >> >> references for this? >> >> >> >> >> >> --linas >> >> >> On Tue, Dec 11, 2018 at 2:24 AM Ivan Vodišek <[email protected]> >> wrote: >> >> >> > >> >> >> > 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. >> >> >> >> >> >> >> >> >> >> >> >> -- >> >> >> 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/CAHrUA37GsrK8UWA1yLkH0D1d9msCT_pgSenWCqzvdcU2K6zZ4w%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%3Dj6VrJ%2BH_GZHPNy%3DA4yjdB5hN10oOCAJ1KNu2Q6PzdxQ-_w%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/CAHrUA34zP3MSpWxJv750ScsGFVT_3-V6K13cj0_Dw6GV5rQXJA%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%3Dj6XiNjDz2TwRdmrRO_%2BAPMN95nxCJpj8MYNDiLp%2BL3aong%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/CAHrUA34T7UidSED_vUHxy0T4%3DGL9N3uO6NwRP4j_k6N-SfGh6A%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%3Dj6V4pUpK6_ccryUr4VBncJ3F-0w-_hcT0_XQJtP1f%2BiYMw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
