The connection is the following (using Hilbert's direction):
* (cause / string-of-terminals-or-non-terminals-to-be-parsed) *->*
(consequence / match-pattern)
With a help of common rules (again in Hilbert System):
* A *->* (A \/ B)
* B *->* (A \/ B)
Proving is performed from left to right, while parsing is performed from
right to left. Considering Curry-Howard-Lambek
<https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence>
correspondence, I suppose we may add unrestricted grammars to it also.
Unrestricted grammars are anyway considered Turing machine equivalent
<https://en.wikipedia.org/wiki/Unrestricted_grammar#Equivalence_to_Turing_machines>
rewriting <https://en.wikipedia.org/wiki/Rewriting> mechanisms, so this
should be no surprise at all, although I didn't imagine it would be that
simple and straightforward.
If anyone is interested in serious parser/proof material written by
professionals, there is excellent Stanford's Introduction to Logic
<http://intrologic.stanford.edu/public/index.php>. Chapter 9.6 - Pseudo
English
<http://intrologic.stanford.edu/public/section.php?section=section_09_06> covers
a kind of context free grammars implemented in logic, and we should be
able to extended it to unrestricted grammars also.
Stay cool,
Ivan V.
pon, 17. pro 2018. u 12:32 Zar Goertzel <zar...@gmail.com
<mailto:zar...@gmail.com>> napisao je:
Briefly asked Chad the logic guru.
He says sounds like the proof-logic for parsing would be something
in the linear logic direction. Mentions Lambek and
https://en.wikipedia.org/wiki/Grammatical_Framework.
But he isn't sure something as detailed/formal as you'd like has
been done yet...
On Fri, Dec 14, 2018 at 12:27 PM Zar Goertzel <zar...@gmail.com
<mailto:zar...@gmail.com>> wrote:
Howdy Linas,
Unfortunately, I'm drastically ignorant compared to my senior
colleagues and you.
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"?
We had happened to be talking about it at lunch when you brought
that up. It seems likely they're in a similar state to you: it
seems obvious and they can wave their hands around, but haven't
bothered formally writing it up.
Would it be hard to write up formally?
On Wed, Dec 12, 2018 at 1:17 AM Linas Vepstas
<linasveps...@gmail.com <mailto:linasveps...@gmail.com>> wrote:
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?
The logic of term rewriting is paramodulation? That's not a
modal logic though . . .
--linas
On Tue, Dec 11, 2018 at 2:24 AM Ivan Vodišek
<ivan.mo...@gmail.com <mailto:ivan.mo...@gmail.com>> 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
<linasveps...@gmail.com <mailto:linasveps...@gmail.com>>
napisao je:
>>
>> On Sun, Dec 9, 2018 at 11:55 AM Ivan Vodišek
<ivan.mo...@gmail.com <mailto:ivan.mo...@gmail.com>> 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
opencog+unsubscr...@googlegroups.com
<mailto:opencog%2bunsubscr...@googlegroups.com>.
>> To post to this group, send email to
opencog@googlegroups.com <mailto:opencog@googlegroups.com>.
>> 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
opencog+unsubscr...@googlegroups.com
<mailto:opencog%2bunsubscr...@googlegroups.com>.
> To post to this group, send email to
opencog@googlegroups.com <mailto:opencog@googlegroups.com>.
> 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 opencog+unsubscr...@googlegroups.com
<mailto:opencog+unsubscr...@googlegroups.com>.
To post to this group, send email to opencog@googlegroups.com
<mailto:opencog@googlegroups.com>.
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/CAHY-%3DHEmBKgtJPAeKTXAOyOaE4gR8cZeouc8v9JhQb3E4jX%2BkQ%40mail.gmail.com
<https://groups.google.com/d/msgid/opencog/CAHY-%3DHEmBKgtJPAeKTXAOyOaE4gR8cZeouc8v9JhQb3E4jX%2BkQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.
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 opencog+unsubscr...@googlegroups.com
<mailto:opencog+unsubscr...@googlegroups.com>.
To post to this group, send email to opencog@googlegroups.com
<mailto:opencog@googlegroups.com>.
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%3Dj6XXTvSx_BCNHsS-CSfzCjH2y0MeedeepUY_%2B5ANx-h99g%40mail.gmail.com
<https://groups.google.com/d/msgid/opencog/CAB5%3Dj6XXTvSx_BCNHsS-CSfzCjH2y0MeedeepUY_%2B5ANx-h99g%40mail.gmail.com?utm_medium=email&utm_source=footer>.
For more options, visit https://groups.google.com/d/optout.
