stuck with infinity

[Ivan Vodišek]

So i have an expression definition language. besides that come rules in pattern matching manner like:

<a> * <x> + <a> * <y> => <a> * (<x> + <y>)

Upon stating a starting set of expressions all rules are matched against that set and against themselves to enrich starting set with new expressions. I would call that as deduction.

The problem is with rules like

<x:Number> => <x> + 1

When resulting right side is reconsidered with the left side of the same rule, a new statement is produced, but that statement also matches left side which goes to infinity. Something like:

<x> + 1 + 1 + 1 + ...

I would like to detect rules like this one and report them as errors, as they should be rewritten nonrecursively like:

<x:Number> => <x> + 1 [N times]

with right side of type "function of N"

When left side is consisted only of one variable, all I have to do is to match right side against left side to detect unwanted behavior, but I don't know if there are other cases that lead to infinite calculation.

Are there other cases or this is it? Maybe someone already encountered the same problem? Do U have any idea on how to resolve this?

If so, I would like to hear Ur thoughts.

[SeH]

maybe what you're describing is called Mathematical Induction?

http://en.wikipedia.org/wiki/Mathematical_induction

not sure of any algorithms for it but there may be some.

for matching expressions, which are probably best represented as trees, you may want to look into something like "subgraph mining":

http://wiki.opencog.org/w/New_Fishgram_Design,_2013

since trees are a subtype of graph.  in opencog's case it ought to be able to find similar expressions between Combo programs:

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

correct me if i'm wrong ivan, i may not be understanding the problem 100%

--
You received this message because you are subscribed to the Google Groups "Genifer" group.
To unsubscribe from this group and stop receiving emails from it, send an email to general-intellig...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ivan Vodišek]

It is basically pattern matching on whatever expressions, being math, logic, or anything else. There are possible expression definitions and a set of transformation rules. Program starts with a set of manually entered beginning expressions. When these expressions are found in left side of transformation rules (pattern matching), new expressions (right sides of rules) are being populated to starting set, making the set richer by new conclusions. I think that this reflects usual human thinking process and it is pretty simple solution.

The problem is that some rules can be repetitively applied on their very results, making an infinite loop, and I would like to detect these rules. Maybe the solution is to pattern match whole right side expression against whole left side pattern and if it passes, an error can be reported.

[Matt Mahoney]

Isn't solving rewriting rules in general equivalent to solving the
halting problem? For example, the Collatz sequence:

<x> => <x> * 3 + 1 if x is odd
<x> => <x> / 2 if x is even

This terminates at the repeating loop 4 2 1 4 2 1 ... for all known
positive integers x that have been tested, but nobody knows if there
are some other x that terminate at other cycles or grow to infinity.

-- Matt Mahoney, mattma...@gmail.com

[Ivan Vodišek]

To avoid infinite loop, the case of Collatz sequence would be rewritten as:

Collatz (

    x {@Int}

    next {

        @Collatz (

            x <

                <Collatz.x> is odd  => <Collatz.x> * 3 + 1

                <Collatz.x> is even => <Collatz.x> / 2

            >

        ) |

       @Null

    }

)

Now it terminates upon

Collatz <x <1>>

because "next" would be lazy evaluated. Specific elements would be retrieved from outer invoker by

Collatz <x <1>>.next.next.next...

With "next" being repeated N times regarding to outer invoker's reasoning call.

I think it could work.

[Matt Mahoney]

But do you know if all values of x eventually return 1?

[Ivan Vodišek]

sorry, I have no clue about that

[Ivan Vodišek]

to know that, it would require a proof that all values of x eventually return 2 to the power of N. In that case the number is reduced to 1 due to rule

<x> => <x> / 2 if x is even

maybe that could be a starting point, but I doubt it would produce some result.

[Ivan Vodišek]

I think that problem with infinite sets is that total induction can not be practiced so there might exist things that can not be proved.

[Matt Mahoney]

Conway proved that a class of Collatz like problems are undecidable,
although not the Collatz problem specifically.
http://mathworld.wolfram.com/CollatzProblem.html

[Ivan Vodišek]

Well, some of problems with infinite sets are provable. For mathematical series all U need to prove is

f(x) = some y

and

f(x + 1) = the same y