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]
<mailto:[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]
<mailto:[email protected]>> napisao je:
On Wed, Dec 12, 2018 at 2:28 AM Ivan Vodišek
<[email protected] <mailto:[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] <mailto:[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] <mailto:[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] <mailto:[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] <mailto:[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] <mailto:[email protected]>> napisao je:
>> >> >>
>> >> >> On Sun, Dec 9, 2018 at 11:55 AM Ivan Vodišek
<[email protected] <mailto:[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]
<mailto:opencog%[email protected]>.
>> >> >> To post to this group, send email to
[email protected] <mailto:[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]
<mailto:opencog%[email protected]>.
>> >> > To post to this group, send email to
[email protected] <mailto:[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]
<mailto:opencog%[email protected]>.
>> >> To post to this group, send email to
[email protected] <mailto:[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]
<mailto:opencog%[email protected]>.
>> > To post to this group, send email to
[email protected] <mailto:[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]
<mailto:opencog%[email protected]>.
>> To post to this group, send email to
[email protected] <mailto:[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]
<mailto:opencog%[email protected]>.
> To post to this group, send email to [email protected]
<mailto:[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]
<mailto:opencog%[email protected]>.
To post to this group, send email to [email protected]
<mailto:[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]
<mailto:[email protected]>.
To post to this group, send email to [email protected]
<mailto:[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
<https://groups.google.com/d/msgid/opencog/CAB5%3Dj6V4pUpK6_ccryUr4VBncJ3F-0w-_hcT0_XQJtP1f%2BiYMw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
For more options, visit https://groups.google.com/d/optout.
