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... But this one is linear, as described. 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).
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
)
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 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.
