New design philosophy

One trend I begin to spot is that people often have somewhat divergent desires of what features they want their AGI brain children to have.  So, maybe the philosophy of our project is to let many AGI developers to draw from a common pool of algorithms, techniques, code, gadgets, etc, to DIY.  "No Child Left Behind - 2".

( "No Child Left Behind - 1" is that we cater to both Java and .NET platforms.  OpenCog takes care of C++ so we don't need to worry about that.  And, on the native scene there are some very good languages like Haskell and Erlang, but they don't have a large enough user base to warrant forking a 3rd branch.  )

Cobra implementation of Logic class

This is Chuck's code in Cobra.  I'm still examining it....
============================================================

http://www.pastey.net/138443-2v9q

implementation: the "Logic" class

Definition of the Logic class:

Formula------------ Constant ------------------------ Atom
                |                                          |
                --------- Variable                  ---------- Char, and String
                |                                          |
                --------- Apply-Operator       ---------- Number ------------ Integer, Real, Bool, etc...
                |                                                                        
                --------- Apply-Functor


Atom:  {  string: name,  int: index  }                                 // atoms are eg: "john", "mary"
Variable:  {  int: index  }
Apply-Operator:  {  char: op,  Formula[]: arguments  }          // op applied to 1 or more arguments
Apply-Functor:  {  Atom: functor, Formula[]: arguments  }    // functor applied to 1 or more arguments
                                                                                      // functor can be function or predicate
                                                                                      // functor's name is just an Atom

Definition of FOL terminology:

This set of terminology is standard for FOL:

1. At the top level is the formula (or proposition, or sentence, or logic statement, all synonyms).
2. A formula can be a rule or a fact.  A rule is of the form
        A <- X, Y, Z, ...
   And a fact does not contain the "<-" operator.
3. Each formula consists of a number of literals joined by logical operators (aka connectives) such as AND and OR, and operations can be nested.  Note that NOT is a unary operator.  Eg:
• (loves john mary)                                     is a literal
• (NOT (female john))                                is a literal
• (AND (loves john mary) (female mary))    are 2 literals joined by AND
• (OR (AND (p X) (q Y))  (r Z))                  is nested
4. Each literal consists of a predicate plus its arguments, eg:
• (loves john mary)                    where love = predicate with 2 arguments
• (male paul)                             where male = predicate with 1 argument
• (female (daughter-of paul))      where female = predicate with 1 argument, "daughter-of" is a function symbol
5. Terms (or arguments) can be:
• variables   (eg:  X, Y, Z)
• constants   (eg:  john, mary, 17, "String")
• functions of other terms   (eg:  daughter-of(john),  sine(3.14))

That's all!

Our simplified terminology:

In anticipation of higher-order logic:

1. The notion of predicates and functions are combined into functors.
2. We can also absorb functors into operators, but this is not currently done.
3. In FOL, a function-application is not a formula, but this is relaxed in our definition.  Potentially it can lead to ill-formed formulas.  For example, sine(3.14) is clearly not a formula;  but we want to allow some functions that return formulas.

The result is more elegant, and we can express this by a set of re-write rules:
     formula ===> constant
     formula ===> variable
     formula ===> (functor formula1 formula2 ...)
     formula ===> (op formula1 formula2 ...)

More about rules

Rules are of the form:

     A <- B, C, D, ...

where A is the "head", B,C,D,... is the "body", and "<-" is just a special operator like "AND";  we can call it "COND" for conditional.

Each "," is equivalent to an "AND".  So, the above rule is represented as:

     (COND A (AND B C D...))

where "AND" can accept more than 2 arguments.

( In our logic, <- translates to a link in a Bayesian network.  For this reason, it seems not very meaningful for a formula to have "<-" inside the body instead of at the head position. )

Some special cases:

1. If a rule has no head, it is still a rule, such as:
        (interesting X)    means "everything is interesting"
   -- note that all variables are implicitly universally quantified, ie, the above is really:
        for-all X,  interesting X
2. We can ignore the case where a rule has no body (it's not useful).
3. A rule without variables is still a rule, eg:
        wet <- rains
        not cloudy <- sunny

Representing variables and constants

Notice that we can use any way we want to represent variables and constants internally.  In my Lisp code, variables are like "?1" etc and constants are "john" etc.  In a more sophisticated KB, we would of course use some kind of indexes.

Code

This is Russell's C# code, and Chuck's Cobra code.  When in doubt, please conform to the definition above.

basic English

This is a basic English lexicon for talking about things in programming.  It seems to get quite large as I think of more and more words to add to it, and I'm not sure if it's too big for the prototype to handle.  For the grammar we can modify the simple English grammar in PAIP.

nouns:

function, program, procedure

number, integer, real

memory, variable, pointer, constant, value, content

data, structure, input, output

list, queue, tree, stack, node, link

loop, iteration

verbs:

add, subtract, multiply, divide

increase, decrease, increment, decrement

move, link, compare

create, delete, update, change, fix, set, assign

open, close, enter, exit

input, output

adjectives:

free, open, closed

fast, slow, simple, complex, hard, easy

big, small, long, short, deep, shallow, broad, narrow

propositions:

on, by, to, in, of, for, with, within, without, against

conjunctions:

if, then, while, for

and, or, not

pronouns, etc:

I, you, he, she, it, they, them, him, his, her, mine, yours

who, what, where, when, how

please, okay, thanks, bye!

reasons for using .NET

Seems that the good candidate languages are only C#, F# and Cobra.

Lacks usable Prolog / Lisp / Haskell implementations (JVM doesn't have Prolog / Haskell either).

reasons for using Java/JVM

Clojure -- .NET lacks a good Lisp implementation.

Scala is OO + functional.

question: is Jython good/fast?

HOL update

YKY doesn't want to focus on HOL at the moment, but he suggested I write down my thoughts anyway. I was going to put it off since I'd really want to do a more detailed write-up taking care of all the loose ends, but since there is some interest from Russel, I'm outlining my approach now.

The approach is to translate system IG from the paper Illative Combinatory Logic. This is an untyped lambda-calculus logic which soundly & completely interprets first-order logic both "directly" (ie, as truth functions) and via curry-howard isomorphism (which indicates the strength of the type reasoning the system can interpret).

The way I'm planning on translating it is to treat a statement and its negation as essentially separate statements in the probability distribution; ie, the Liar sentence can have probability 0, but its negation can simultaneously have probability 0. Only when we know a statement is a proposition can we derive that P(prop) = 1 - P(~prop).

After this, what we do is just encode the valid sequents as rules in our existing logic. However, IG has an infinite number of valid sequents, specified with some sequent derivation rules. This means that we've got an infinite number of rules now-- we need an efficient mechanism for constructing valid rules as they are needed. The sequent derivation rules get turned into "meta-rules" in our logic. This is a bit complicated, but better than the alternatives (see my previous post).

One complication is that sequent-based need to be combined with something like the noisy-or combination rule [I need to add a reference...]. At present we're planning on dealing with this by having noisy-or be the default combination rule in the whole system; there are some cases where it is a terrible rule, though. YKY thinks we can determine which cases to apply it to using causal reasoning.

For efficient reasoning, we'd like to normalize terms before reasoning so that we can quickly recognize equality. However, in untyped HOL, some terms have nonterminating normalizations. There are a few things we can do. One is to just have a time cutoff on normalization attempts. Another is to try and do some type reasoning before normalization (so we'd only normalize when we could first prove termination). A third option that might have some interesting properties is what I'm calling "compressive normalization"... rather than the usual normalization, use the shortest form of a term as the normal form. This is non-terminating and we'd still need a time cutoff, but unlike the usual normal form, it exists even for terms which aren't propositions-- it just always exists. It might be useful to keep short forms of terms around for compression purposes.

Speaking of compression; integrating both HOL and likelihood reasoning into Gen means that might be feasible to specify a prior probability distribution over models within Gen itself, meaning iduction just becomes probabilistic deduction. However, I have not worked out details here.

That's all for today! :)

HOL, Paradox Free: a plan of attack, or two.

Looking at the Illative Combinatory Logic paper today, and thinking about paradox-free HOL.

There are plenty of paradox-free HOLs out there. The question is, how do we translate them into our system? Most HOLs seem to be described in sequent calculus. This means the system has an extra meta-level that ours lacks: it's not really specified as a system for reasoning about HOL statements; rather, it's specified as a system for reasoning about HOL proofs. This means there are at least 3 levels at which the translation can be made: (H) we could try to use the sequent derivation rules as rules in our system, (M) we could use the sequents themselves as rules in our system, and (L) we could use the conditional statements of the HOL as our rules. (I'm labeling these as High, Medium, and Low, in case you're wondering what the letters stand for.)

H might be easiest in that it would only require a finite number of rules to be added to the system. However, it would mean making room for sequents as a type of statement in the system, which could be awkward. We would still want to be able to make basic statements, ie, statements about actual things rather than just about what follows from what... so we would need to also add rules for using sequents to derive base facts from one another. On top of all this, we need to worry about how the probabilistic reasoning is done. It seems that the sequent reasoning would end up being crisp, which means the probabilistic reasoning would only happen when we applied sequents to uncertain base-statements. Again, this seems awkward.

M would require an infinite number of rules, meaning that we'd have to implement rule-level reasoning to derive new rules as they are needed. I discussed rule-level reasoning before; the additional sequent-derivation rules would have to be integrated with my earlier thoughts. For the most part, I think this would mean restricting my earlier suggestion to make sure that it's consistent for the same reasons the sequent rules are consistent. Figuring out the maximum level of rule-level reasoning I can preserve may be difficult. Figuring out the minimum level that's sufficient probably won't be, though! What would be somewhat difficult would be generalizing the backwards-chaining reasoner to create new rules for itself to backwards-chain on (in a sorta meta-backwards-chaining way).

L would require a doubly infinite number of rules (so to speak). The approach would again require rule-level reasoning, but this time rather than implementing a finite number of meta-rules (based on the rules for deriving new sequents) we'd appear to need an infinite number, specified by a finite number of meta-meta rules. This is obviously too much; so, we'd have to pull back and instead figure out a system which satisfied the constraints laid down by the sequent rules. In other words, we treat the sequent-calculus description of the logic as a specification of target features rather than a description of the deduction rules of a system. This is obviously a more difficult approach... an interesting challenge, but more difficult.

Also worth a mention: a tempting, but probably incorrect direction: merge the levels so that we don't have to deal with so many. We'd start allowing conditionals to compose with other language elements, like in regular FOL, so that we can have stuff like A->(B->C). We'd then try to use regular reasoning to implement all the different levels at once. This sounds powerful, but it would probably just create an inconsistent system, defeating the point.




Conclusion

Approach M seems to be the best plan, so I will get to work on that!

Porting Genifer LISP to Scala or Clojure, July 1st

Per YKY's instructions, I am getting ready to port Genifer's existing LISP code located at...

http://launchpad.net/genifer

...to either Scala or Clojure, JVM languages which can inter-operate with Java.  In doing this I hope to provide a framework that will ultimately unify AI libraries like Genifer, dANN, Neuroph, and others.


_KY_: The porting is 3 steps:

1. unification algorithm
• this contains a "unify" written in Haskell:
  http://propella.blogspot.com/2009/04/prolog-in-haskell.html
2. best-first search
3. substitution management
4. optional: [ forward chaining ]
5. optional: [ abduction ]

YKY recommends that I review:

• the target language
• the 2 chapters about logic and inference from "Artificial Intelligence: A Modern Approach"
• the Genifer slides on Deduction which explains YKY's LISP code in a very detailed way

Code will be commited to Genifer's Google Code repository.