Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make rule implicand explicit for the backward chainer #119

Closed
ngeiswei opened this issue Jun 30, 2015 · 35 comments
Closed

Make rule implicand explicit for the backward chainer #119

ngeiswei opened this issue Jun 30, 2015 · 35 comments

Comments

@ngeiswei
Copy link
Member

The backward chainer needs to know the structure of its implicand in order to select the applicable rules of a target. The problem is that given the way rules are currently represented, the implicand does not need to be explicit. Given the following format

BindLink
   AndLink
      <Implicant>
   <Implicand>

Implicand is usually hidden in an ExecutionOutputLink like

ExecutionOutputLink
   "scm:compute-the-implicand"
   ListLink
      ARG1 ... ARGn

Currently the backward chainer looks at ARG1 to ARGn to guess the implicand, but nothing guaranties that this guess is correct, ARG1 to ARGn may turn out not to represent the implicand at all. Besides, even when the implicand is in there, the rule is harder to filter due to the other arguments which are not the implicand (@williampma correct me if I'm wrong).

We need to set an additional constraint on the rule format to make the implicand explicit. I think ideally we'd use a SetTVLink, see below.

Let's assume SetTVLink has the following format

SetTVLink
   <Atom>
   <TV>

So this would assign to . It's not clear what should be, it could be a TVLink that takes 2 NumberNode arguments, or something like that, anyway.

The rule would have the following format

BindLink
   <Variables> (optional)
   <Implicants>
   SetTVLink
      <Implicand>
      <TV>

For instance a deduction rule would look like

BindLink
   AndLink
      ImplicationLink
         VariableNode "$A"
         VariableNode "$B"
      ImplicationLink
         VariableNode "$B"
         VariableNode "$C"
   SetTVLink
      ImplicationLink
         VariableNode "$A"
         VariableNode "$C"
      ExecutionOutputLink
         GroundedSchemaNode "scm:deduction-formula"
         ListLink
            ImplicationLink
               VariableNode "$A"
               VariableNode "$B"
            ImplicationLink
               VariableNode "$B"
               VariableNode "$C"

the scheme code deduction-formula would still need to take Implication(A B) and Implication(B C) to get their TVs and compute the TV of Implication(A C).

If we don't want to wait for SetTVLink, we could still use that format replacing SetTVLink by ExecutionOutputLink + some scheme code, like

BindLink
   AndLink
      ImplicationLink
         VariableNode "$A"
         VariableNode "$B"
      ImplicationLink
         VariableNode "$B"
         VariableNode "$C"
   ExecutionOutputLink
      GroundedSchemaNode "scm:set-tv"
      ListLink
         ImplicationLink
            VariableNode "$A"
            VariableNode "$C"
         ExecutionOutputLink
            GroundedSchemaNode "scm:deduction-formula"
            ListLink
               ImplicationLink
                  VariableNode "$A"
                  VariableNode "$B"
               ImplicationLink
                  VariableNode "$B"
                  VariableNode "$C"

Slightly more verbose but allows to move on without having to define SetTVLink. Although I think taking the time to implement Set/Get TV links would be a good thing.

Also in both cases we could define some scheme function to build the BindLink given the rule's implicants, implicand and formula code. Or maybe store it that way, and let the URE build the BindLink as appropriate.

@williampma
Copy link
Member

This looks to be the same problem mentioned in opencog/opencog#1441 and opencog/opencog#1593

Note that explicitly defining the output (implicand) of a rule is not always possible. Some rules could generate an infinite possible output (bases on some outgoing set of an input link, for example). I recall @bgoertzel wrote a solution (requiring some special yet to be invented system I recall). I couldn't find it at the moment (is it on google group or wiki... can't remember...)

@ngeiswei
Copy link
Member Author

Maybe we don't need to have a single rule that expressive (generate an infinite possible output). We can always generate multiple simple rules via some scheme code, right?

@amebel
Copy link
Contributor

amebel commented Jun 30, 2015

@bgoertzel
Copy link
Contributor

Yeah. I thought the best way to solve this problem was to introduce the
"deep type system" i.e. "haskell or haskell-ish type system" suggested by
Nil previously.... If the rule output has a type associated with it, then
backward chaining can be done based on the type

On Tue, Jun 30, 2015 at 11:15 PM, Amen Belayneh notifications@github.com
wrote:

http://wiki.opencog.org/w/Deep_types


Reply to this email directly or view it on GitHub
#119 (comment).

Ben Goertzel, PhD
http://goertzel.org

"The reasonable man adapts himself to the world: the unreasonable one
persists in trying to adapt the world to himself. Therefore all progress
depends on the unreasonable man." -- George Bernard Shaw

@ngeiswei
Copy link
Member Author

Deep type alone cannot fix the problem, we still need a way to tell "this is the implicand", and currently, as far as I can tell we don't have one, do we? Or is there already a convention regarding the arguments of the ExecutionOutputLink, like the first arg is the implicand (as suggested by @misgeatgit I believe)?

@bgoertzel
Copy link
Contributor

Hmmm... I think there may be a couple problems mixed up here...

Is one problem that you removed the ImplicationLink from inside the
BindLink??

Of course, a PLN rule needs an ImplicationLink --- it is, logically, an
implication!!!

A rule needs to be of the form

ImplicationLink
Premises
Function for generating conclusions

Not all BindLinks need to involve ImplicationLinks, but PLN rules do

I see, you may be right that deep type alone is not enough..... Knowing
the type of a conclusion, doesn't necessarily tell you enough to infer if
some other rule is able to take that conclusion as a premise.

I wonder if we could express a rule something like

ImplicationLink
Premises
Output of function for generating conclusions

(optional)
XXXLink (see below)
Output of function for generating conclusions
Template describing nature of output

...

The "template" would be an Atom-structure suitable for matching/chaining.

For instance, the rule Evaluation2Member(*,k)

described at

http://wiki.opencog.org/w/Deep_types

would look like

ForAllLink $D, $L, $k
Implication
Evaluation
$D
$L
Member [123]
ExecutionOutputLInk
GSN “ElementAt”
ListLink
ListLink $L
NumberNode $k
SatisfyingSet
Variable $V
ExecutionOutputLink
GSN “Insert”
ListLink
ListLink $L
Variable $V
NumberNode $k

ThereExists $X, $Y [456]
EquivalenceLink
[123]
Member
ConceptNode $X
ConceptNode $Y

EvaluationLink
PredicateNode "OutputTemplate"
[123]
[456]

...

The output template would then be used for chaining, and the actual output
generation function [123] produces the specific output fitting into the
template...

-- Ben

On Wed, Jul 1, 2015 at 4:26 AM, ngeiswei notifications@github.com wrote:

Deep type alone cannot fix the problem, we still need a way to tell "this
is the implicand", and currently, as far as I can tell we don't have one,
do we? Or is there already a convention regarding the arguments of the
ExecutionOutputLink, like the first arg is the implicand (as suggested by
@misgeatgit https://github.com/misgeatgit I believe)?


Reply to this email directly or view it on GitHub
#119 (comment).

Ben Goertzel, PhD
http://goertzel.org

"The reasonable man adapts himself to the world: the unreasonable one
persists in trying to adapt the world to himself. Therefore all progress
depends on the unreasonable man." -- George Bernard Shaw

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 1, 2015

@bgoertzel Adding the ImplicationLink back in the BindLink wouldn't add any new information, would it? Regardless of whether removing the ImplicationLink from BindLink was a bad idea, it seems independent of that problem.

Maybe I haven't been clear enough, the problem is that currently the formula, which is a black box, doesn't just take care of the TV but also of the whole output, so there is no way, unless the black box is run to get the output pattern. Your example about deep type is a good one, but completely ignores that issue, and the deep type does not reflect the shallow type (the syntactic hypergraph structure) we also want. I guess we want both shallow and deep type checkers that can run over the scheme code black box, it seems difficult to implement (we'd have to fiddle with scheme semantics), but it would indeed be the answer. Surely Shallow + Deep types contain all the information we need to perform the pattern matching on the target so select the rule! Or at least it's good enough (not getting into dependent types).

Now till we get good shallow and deep type checkers we still want to be able to run the backward chainer, there is definitely a lot of development to be done on it and I don't think we should postpone URE development till we get good type checkers.

So meanwhile what I suggest is to come up with a convention to get that output structure. The SetTVLink is a clean way to split that black box into a clear box part and a black box part containing only the formula, and therefore let the output structure visible. There are other ways. In the absence of other suggestions I'll probably settle with @misgeatgit 's, like the first argument of the formula black box must be the output.

I suggest that as soon as the URE is working "well enough", we can start working on the type system.

@bgoertzel
Copy link
Contributor

On Wed, Jul 1, 2015 at 3:57 PM, ngeiswei notifications@github.com wrote:

@bgoertzel https://github.com/bgoertzel Adding the ImplicationLink back
in the BindLink wouldn't add any new information, would it?

Using an ImplicationLin here would just make the Atomspace formulation of
PLN rules semantically correct...

An inference rule IS an implication: premises IMPLY conclusions, and the
current Atomspace formulation does not reflect this...

I don't think ImplicationLInks are ALWAYS needed with BindLinks, but in
this case, we really really do have a probabilistic-logical Implication, no?

Maybe I haven't been clear enough, the problem is that currently the
formula, which is a black box, doesn't just take care of the TV but also of
the whole output, so there is no way, unless the black box is run to get
the output pattern. Your example about deep type is a good one, but
completely ignores that issue, and the deep type does not reflect the
shallow type (the syntactic hypergraph structure) we also want.

Yes, but my "OutputTemplate" does address this -- the output template IS
the "syntactic hypergraph structure", isn't it?

Now till we get good shallow and deep type checkers we still want to be

able to run the backward chainer, there is definitely a lot of development
to be done on it and I don't think we should postpone URE development till
we get good type checkers.

Agreed

So meanwhile what I suggest is to come up with a convention to get that
output structure. The SetTVLink is a clean way to split that black box into
a clear box part and a black box part containing only the formula, and
therefore let the output structure visible. There are other ways. In the
absence of other suggestions I'll probably settle with @misgeatgit
https://github.com/misgeatgit 's, like the first argument of the
formula black box must be the output.

I suggest that as soon as the URE is working "well enough", we can start
working on the type system.

Agree on both points...

ben

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 1, 2015

On 07/01/2015 11:04 AM, bgoertzel wrote:

On Wed, Jul 1, 2015 at 3:57 PM, ngeiswei notifications@github.com wrote:

@bgoertzel https://github.com/bgoertzel Adding the ImplicationLink back
in the BindLink wouldn't add any new information, would it?

Using an ImplicationLin here would just make the Atomspace formulation of
PLN rules semantically correct...

An inference rule IS an implication: premises IMPLY conclusions, and the
current Atomspace formulation does not reflect this...

I don't think ImplicationLInks are ALWAYS needed with BindLinks, but in
this case, we really really do have a probabilistic-logical Implication, no?

Well, the ImplicationLink can definitely have a valid PLN interpretation
(although the TV on the ImplicationLink, or its quantifier, would need
to be properly computed), and surely this would be a valuable knowledge
for OpenCog to reason about its own reasoning process. Other than that I
don't think it is needed, it certainly isn't for the URE to work
properly. The day we need to have OpenCog to reason about its own
reasoning process, we can build those ImplicationLinks.

Maybe I haven't been clear enough, the problem is that currently the
formula, which is a black box, doesn't just take care of the TV but
also of
the whole output, so there is no way, unless the black box is run to get
the output pattern. Your example about deep type is a good one, but
completely ignores that issue, and the deep type does not reflect the
shallow type (the syntactic hypergraph structure) we also want.

Yes, but my "OutputTemplate" does address this -- the output template IS
the "syntactic hypergraph structure", isn't it?

Sure, it is. I mean that in case the output template is hidden, a
shallow type engine could infer it back, that could be cool.

Nil

Now till we get good shallow and deep type checkers we still want to be

able to run the backward chainer, there is definitely a lot of
development
to be done on it and I don't think we should postpone URE development
till
we get good type checkers.

Agreed

So meanwhile what I suggest is to come up with a convention to get that
output structure. The SetTVLink is a clean way to split that black
box into
a clear box part and a black box part containing only the formula, and
therefore let the output structure visible. There are other ways. In the
absence of other suggestions I'll probably settle with @misgeatgit
https://github.com/misgeatgit 's, like the first argument of the
formula black box must be the output.

I suggest that as soon as the URE is working "well enough", we can start
working on the type system.

Agree on both points...

ben


Reply to this email directly or view it on GitHub
#119 (comment).

@bgoertzel
Copy link
Contributor

Well, the ImplicationLink can definitely have a valid PLN interpretation
(although the TV on the ImplicationLink, or its quantifier, would need
to be properly computed), and surely this would be a valuable knowledge
for OpenCog to reason about its own reasoning process. Other than that I
don't think it is needed, it certainly isn't for the URE to work
properly. The day we need to have OpenCog to reason about its own
reasoning process, we can build those ImplicationLinks.

I dunno... having the rules represented in such a semantically opaque
format just seems wrong to me.... I understand it won't stop the URE from
working but eventually it will bite us in the ass somehow...

I guess I'll have to think more about whether this reformulation of the
rules is merely inelegant and morally offensive ;), or actually going to be
problematic in the mid-term future... Hmm...

Anyway, I agree this is not the most urgent problem. Getting the chainer
working is certainly more important. But after that, I personally would
like to see the rules represented in a semantically transparent way...

Maybe I haven't been clear enough, the problem is that currently the
formula, which is a black box, doesn't just take care of the TV but
also of
the whole output, so there is no way, unless the black box is run to
get
the output pattern. Your example about deep type is a good one, but
completely ignores that issue, and the deep type does not reflect the
shallow type (the syntactic hypergraph structure) we also want.

Yes, but my "OutputTemplate" does address this -- the output template IS
the "syntactic hypergraph structure", isn't it?

Sure, it is. I mean that in case the output template is hidden, a
shallow type engine could infer it back, that could be cool.

True. But it might be inefficient for the type engine to have to infer it
each time, right? So the OutputTemplate would be a cache...

ben

@amebel
Copy link
Contributor

amebel commented Jul 1, 2015

@ngeiswei

  • how will the new schema for rules solve the black-box issue for Evaluation2Member rule, let say with a predicate having 2 or 3 arguments?
  • What is the semantics of SetTVLink?

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 1, 2015

On 07/01/2015 12:29 PM, Amen Belayneh wrote:

@ngeiswei https://github.com/ngeiswei

  • how will the new schema for rules solve the black-box issue for
    Evaluation2Member rule, let say with a predicate having 2 or 3
    arguments?

It doesn't. You'd still need to split that complex rule into multiple
simpler ones. I think it's OK because ultimately you don't need a very
large number of them, say 3 or 4, maybe up to 10 in a distant future.
And one can easily write some scheme code that would generate them all
up to a certain N.

So if it doesn't solve that, what does it solve? It replaces the current
code that assumes any argument of the ExecutionOutputLink can be the
output by something else so that only one output, the correct one, is
assumed.

  • What is the semantics of SetTVLink?

SetTVLink
Atom
TV

assigns truth value TV to atom Atom and returns Atom.

This would be cool, I might implement it, but we can also assume that
the first argument of the implicand ExecutionOutputLink is the output.
The other option is to replace SetTVLink by ExecutionOutputLink "scm:
cog-set-tv!", it's cooler but more verbose.

BTW, IMO the main semantical opacity comes from the black box scheme
code, SetTVLink is a step towards turning this black box into a clear box.

Hmm, SetTVLink should be pretty easy to implement, maybe I'll do that
tomorrow.

Or alternatively a rule would be defined as a triplet

(Implicant, Implicand, TV formula)

Maybe that would be better, it's very terse and can be turned into
whatever you need. Or a scheme function that given this triplet (as say
3 scheme arguments), turn that into a rule.

So 5 options:

  1. Use 1st arg of the implicand's ExecutionOutputLink as output
  2. Use SetTVLink
  3. Use another ExecutionOutputLink + cog-set-tv!
  4. Use a triplet (Implicant, Implicand, TV formula)
  5. Use scheme code to generate rules given that triplet

If I were the only one working on OpenCog I would probably go with 5
(for the user), then go with 3 (for the algorithm).

Let me know what you think. Ultimately multiple choices are possible. We
could support 1 in the case of black box for the existing rules. And
support 3 and 5 for new rules.

However I would definitely not stay in the current situation where any
argument is assumed to be output.

Or I can implement SetTVLink and convert all existing rules to follow
that format, which would be both clean and terse.


Reply to this email directly or view it on GitHub
#119 (comment).

@williampma
Copy link
Member

Thinking ahead, which solution (1-5) will work best when the DeepType system is eventually implemented (so that when that is implemented, the effort here won't be wasted)?

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

But the deep type system isn't gonna fix all the issues, it's not gonna reveal an output structure hidden in a scheme function. I think the best solution is to use 2+5, but meanwhile 3+5 prevents from implementing a SetTVLink. I'll see how the existing rules can fit into 1, if they easily can maybe I'll go that way.

@williampma
Copy link
Member

True, but it is still part of "showing the true rule's output" solution. I am just wondering if any of the solution will became incompatible with the deep type's solution (ie. when deep type's development begin, the developer might end up removing the solution here to get a good representation working for deep type). A representation is needed so both system can coexist I think?

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

Having powerful shallow + deep type systems maybe remove the need for expliciting the output structure, but it certainly wouldn't be in contradiction with using a more transparent description, with SetTVLink for instance.

Anyway, I do understand your concern about investing too much energy into an temporary solution. I'm about to go through all existing rules to see if solution 1 can easily be used, if that is the case we go that way, end of the debate. If that isn't the case, we must think...

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

OK, so here's my report, only looking at PLN rules (I tried to look at relex2logic but the comments were too obscure for me to understand the rules)

Rules with output pattern as first argument

abduction.scm
context-free-to-sensitive.scm
contextualize.scm
decontextualize.scm
equivalence-transformation-rule.scm
evaluation-to-member.scm
inheritance-to-member.scm
member-to-inheritance.scm
modus-ponens.scm

Rules with output pattern as last argument

and-breakdown-rule.scm
and-simplification-rule.scm
and-to-context.scm
and-transformation-rule.scm
deduction.scm
not-elimination-rule.scm
not-simplification-rule.scm
or-breakdown-rule.scm
or-simplification-rule.scm
or-transformation-rule.scm

Rules with no output pattern (hidden in the scheme code)

and.scm
member-to-evaluation.scm
not.scm
or.scm

Rules with multiple outputs

and-elimination-rule.scm
or-elimination-rule.scm

I thinking, there might be another way, more soon...

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

OK, so the problem, and I had not realized that before looking at all these rules, some rules have multiple outputs, I don't know if that's a good idea, but if we really wish to support that, here's my suggestion:

Suggestion

Run the scheme code over the (ungrounded) patterns to unravel the output structure!

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

That way we don't care were the output is, or even if there's one. I think it would work, but we'd need to try to know for sure...

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

Thinking about it, it is a hacky way to infer the output's shallow type. So once we have a shallow type (and ultimately a deep type) system we can drop this hack (if it's gonna work anyway).

@williampma
Copy link
Member

Run the scheme code over the (ungrounded) patterns to unravel the output structure!

Only possible if the scheme code is simple. If the rule matched a variable to a link and the scheme code looks inside the link, then the ungrounded pattern will not have the information.

But may not be a problem for the PLN rules you listed. Just not in general.

@williampma
Copy link
Member

Would it be better to merge @prateeksaxena2809's changes before changing the rule's format?

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

I won't change the rule format, I'll first try the run-scheme-formula hack.

But sure, create a pull request and let's merge it.

@amebel
Copy link
Contributor

amebel commented Jul 2, 2015

I am not sure on which issue that @ngeiswei suggested it, but wouldn't the introduction of regex + and * link and making a modification to the rule definition schema as follows solve black-box rules, for the backward chainer?

(EvaluationLink
     (PredicateNode "output_structure")
     (ListLink
        (ConceptNode "PLN-Evaluation2Member")
        (SignatureLink
            (TypeNode "MemberLink")
            (RegexPlusLink ; this acts on node type, and may inherit from singaturelink
                (TypeNode "VariableNode")
            )
            (SignatureLink
                (TypeNode "SatisfyingSetLink")
                (TypeNode "VariableNode")
                (SignatureLink
                    (TypeNode "EvaluationLink")
                    (TypeNode "PredicateNode")
                    (SignatureLink
                        (TypeNode "ListLink")
                        (RegexStarLink
                            (TypeNode "ConceptNode")
                        )
                        (RegexStarLink
                            (TypeNode "VariableNode")
                        )
                        (RegexStarLink
                            (TypeNode "ConceptNode")
                        )
                    )
                )
            )
        )
    )
)

I am not that privy of regex. Reference http://wiki.opencog.org/w/SignatureLink

@ngeiswei
Copy link
Member Author

ngeiswei commented Jul 2, 2015

@amebel thanks for your input. I actually wasn't aware the pattern matcher's type checker was that advanced (I do understand your regex notation are not implemented, I'm basing that on reading the SignatureLink wiki page).

So yes, a solution could be to specify the shallow type of the output elsewhere, in addition to the rule definition, and have the backward chainer relies on that. That way it wouldn't change the rule format. It would add an extra burden on the user to declare the type though. In order not to add any extra burden to the user the type checker must be able to infer the type's output, I don't think that's currently possible. But anyway, I'm first gonna see if the hack I've lastly suggest would work, if it does, I'll move on to the next issue.

@linas
Copy link
Member

linas commented Mar 27, 2016

is this still an issue?

@ngeiswei
Copy link
Member Author

This still an issue.

@ngeiswei ngeiswei closed this as completed Apr 7, 2016
@bgoertzel
Copy link
Contributor

You implemented your “hack”?
On 7 Apr 2016 4:04 pm, "ngeiswei" notifications@github.com wrote:

Closed #119 #119.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#119 (comment)

@ngeiswei
Copy link
Member Author

ngeiswei commented Apr 7, 2016

It is no longer a hack :-)

Of course the BC itself still requires a major rewrite.

@ngeiswei
Copy link
Member Author

ngeiswei commented Apr 7, 2016

Oh, to answer the question, no I didn't implement the hack consisting to run the GSN with the variables. After exploring a few rules I realized this wouldn't work as William rightly warned. Instead the user has the possibility to specify a number of output patterns.

@bgoertzel
Copy link
Contributor

Hmm. Can you explain more explicitly, maybe with some good example?
On 7 Apr 2016 4:19 pm, "ngeiswei" notifications@github.com wrote:

Oh, to answer the question, no I didn't implement the hack consisting to
run the GSN with the variables. After exploring a few rules I realized this
wouldn't work as William rightly warned. Instead the user has the
possibility to specify the number of output patterns.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#119 (comment)

@ngeiswei
Copy link
Member Author

ngeiswei commented Apr 7, 2016

@bgoertzel I've improved the wiki http://wiki.opencog.org/wikihome/index.php/URE_Configuration_Format#Rule_Definition and added links to examples using only the forward form and both forward and backward forms. Let me know if it's not clear enough.

Of course ultimately with a kick ass deep type checker (such as what we might get by borrowing from Agda's) the backward forms wouldn't be necessary. However till then it is necessary in order to move the BC code forward.

@bgoertzel
Copy link
Contributor

Got it, that's very clear now, thanks ;)

On Thu, Apr 7, 2016 at 7:08 PM, ngeiswei notifications@github.com wrote:

@bgoertzel https://github.com/bgoertzel I've improved the wiki
http://wiki.opencog.org/wikihome/index.php/URE_Configuration_Format#Rule_Definition
and added links to examples using only the forward form and both forward
and backward forms. Let me know if it's not clear enough.

Of course ultimately with a kick ass deep type checker (such what we might
get by borrowing from Agda's) the backward forms wouldn't be necessary.
However till then it is necessary in order to move the BC code forward.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#119 (comment)

Ben Goertzel, PhD
http://goertzel.org

"I am Ubik. Before the universe was, I am. I made the suns. I made the
worlds. I created the lives and the places they inhabit; I move them here,
I put them there. They go as I say, then do as I tell them. I am the word
and my name is never spoken, the name which no one knows. I am called Ubik,
but that is not my name. I am. I shall always be.” -- Ubik

@linas
Copy link
Member

linas commented Apr 15, 2016

There's a fair amount of infrastructure for specifying types. Its mostly unused. it will remain mostly under-developed as long as no one uses it. From what I can tell, the one thing that agda has that atomese doesn't is dependent types. Well, that and I suppose lots of assorted infrastructure; type inference support is weak or unusable depending on what you want to do. I'm convinced that the pattern matcher can do arbitrarily complex type inference. One just has to start experimenting.

The DualLink can be used to search not only for premises, but also for consequents, so could be used to identify backwards-direction rule candidates. The initial implementation doesn't do type checking; I thought about that, and punted, since I figued no one wanted that or used that; but it can be added, and should not be hard.

I'm pretty sure we've got most of the right infrastructure for this kind of stuff, although there are bugs and rough edges and assorted missing bits and pieces.

@bgoertzel
Copy link
Contributor

Interesting. Let us remember to discuss this in depth when you and Nil are
in HK in May...

On Sat, Apr 16, 2016 at 6:42 AM, Linas Vepštas notifications@github.com
wrote:

There's a fair amount of infrastructure for specifying types. Its mostly
unused. it will remain mostly under-developed as long as no one uses it.
From what I can tell, the one thing that agda has that atomese doesn't is
dependent types. Well, that and I suppose lots of assorted infrastructure;
type inference support is weak or unusable depending on what you want to
do. I'm convinced that the pattern matcher can do arbitrarily complex type
inference. One just has to start experimenting.

The DualLink can be used to search not only for premises, but also for
consequents, so could be used to identify backwards-direction rule
candidates. The initial implementation doesn't do type checking; I thought
about that, and punted, since I figued no one wanted that or used that; but
it can be added, and should not be hard.

I'm pretty sure we've got most of the right infrastructure for this kind
of stuff, although there are bugs and rough edges and assorted missing bits
and pieces.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#119 (comment)

Ben Goertzel, PhD
http://goertzel.org

"I am Ubik. Before the universe was, I am. I made the suns. I made the
worlds. I created the lives and the places they inhabit; I move them here,
I put them there. They go as I say, then do as I tell them. I am the word
and my name is never spoken, the name which no one knows. I am called Ubik,
but that is not my name. I am. I shall always be.” -- Ubik

kasimebrahim pushed a commit to kasimebrahim/atomspace that referenced this issue Jul 22, 2020
…thod-without-result-in-gon

Fix segfault on calling method without result
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants