Basis of mathematical deduction

[Gerenuk]

I want to write a program that can do algebraic transformations and mathematical deduction for me. It's not meant to do anything by itself, but rather check the transformations that I do myself for validity. The set of rule I will specify in advance.

I want to capture all/most of the mathematical situations (algebra, operators, multiple equations,...).

So my idea was to store the current state in a tree (http://en.wikipedia.org/wiki/Tree_(data_structure)) with ordered leaves. For example
$$\frac{\mathrm{d}}{\mathrm{d}x}f(x)=ax$$
$$a=2$$
would be represented by

   truth
  /     \ 
 =       =
/  \    /  \
D   *   a  2
|  / \
f  a x
|
x

Then I also need to specify patterns with placeholders and the transformations into which they can be transformed. For example

 D
 |
 +
/ \
x y

can transform to

 + 
/ \
D D
| |
x y

at any position in the expression.

Now I noticed it might be useful to introduce types for the variables (scalar, vector, matrix).

What else do I need to consider to make my system extendable to any maths formalism?

 

[Hurkyl]

Have you done any investigating into formal logic (particularly syntax) yet? It might be worth it.

For your purpose, using trees for your formal language is probably better than using strings, so don't change that.

For your purpose, using types is also probably better than not.



Consider storing "current state" as a set (or list) of trees -- this more closely resembles the general calculus of "from this set of expressions, we deduce this new expression".

(Look up "syntactic entailment" which corresponds to the symbol $\vdash$ and/or look up "logical calculus" or "propositional calculus" or "predicate calculus")



The biggest thing you're missing, I think is some fine detail on types. When I write an expression like

f(a)​

what is its type? Is it a real number computed by plugging the value a into f? Or is it a function in the free variable a? And what about f? Maybe that should be a free variable too!


If you go reading up on formal logic, you'll see people talking about free variables and bound variables. As a specific topic of interest, you might want to look at lambda calculus, which tackles this problem directly. Basically the expression

f(x)​

should have type "real number", and has free variables x (of type "real number") and f (of type "real-valued function of the reals). Differentiating this doesn't make sense!

We turn this into a function by writing

$$\lambda x : f(x)$$​

$\lambda$ is an operator on strings -- it binds the variable x and turns this expression into one of type "real-valued function of the reals". (And with one free variable f of type "real-valued function of the reals") Of course, in this simple case we just have

$$f = \lambda x : f(x)$$​

but this is useful for more complex expressions.


As for your purpose, you obviously wouldn't literally use this. But I think it means each node of your tree has to have some additional bookkeeping information so that you can tell the difference between whether or not the tree

f
|
x

is being used to express a number or being used to express a function.

As an aside, you might consider encoding f(x) instead as the tree

  eval
 /    \
f      x

How to encode differentiation as expressed in a Leibniz style takes some care. Writing d/dx probably binds the variable x as in the lambda calculus. But what type does it return? A function? Or a number? Does it reintroduce x as a free variable?




But maybe I'm just making things complicated, and whatever scheme you had in mind will work out with no problems.

 

[CRGreathouse]

Specifying a collection of transformations sufficient to describe, say, high-school algebra shouldn't be hard. But verifying that two expressions are equivalent given those transformations is probably a difficult task.

I wrote a program similar to what you describe, though it was designed only to differentiate. I quickly found that differentiation was easy, but simplifying expressions was hard. If you include multiple equations, that only makes it harder...

 

[Gerenuk]

Thanks for your detailed thoughts, Hurkyl! I will have a look at the keywords you mentioned. I was aware of some of them, but was hoping someone can point directly to one point I might be missing.

The biggest thing you're missing, I think is some fine detail on types. When I write an expression like

f(a)​

what is its type? Is it a real number computed by plugging the value a into f? Or is it a function in the free variable a? And what about f? Maybe that should be a free variable too!

I'm not sure about the theoretical details you mean (in particular "free variable"). I was planning to make the type of a function outcome dependent on the type of the arguments. So thanks to you I'm noticing this corresponds to a partial evaluation of a function (apply function on the type only).
The simplest case is the addition operation, where the resultant type is the type of the two summands, provided both a constrained to be equal.

Maybe I need to go through the reading you mention, first.

But I think it means each node of your tree has to have some additional bookkeeping information so that you can tell the difference between whether or not the tree

f
|
x

is being used to express a number or being used to express a function.

Good point. I'm getting the picture. I suppose the important point is that you first differentiate with x as a placeholder (free variable?) and only thereafter you are allowed to plug in a value.

As an aside, you might consider encoding f(x) instead as the tree

  eval
 /    \
f      x

That's no restriction on the tree system, but an important issue for the rule. Can you provide arguments why I should prefer this notation?

 

[Hurkyl]

Maybe if I specialize to python semantics, my point will become a little more clear. If E is the mathematical expression "x + a", there are a variety of things we might have really meant:

x = 3.7
a = 4.9

# "x+a" denotes the number which is the sum of x and a
E1 = x + a   

# "x+a" denotes the binary function that adds its
# two dummy arguments
def E2(x, a):
   return x + a

# "x+a" denotes the unary function that adds the global value
# a to its dummy argument
def E3(x):
   return x + a

# "x+a" denotes the unary function that adds the global value
# x to its dummy argument
def E4(a):
   return x + a

def D(f):
   def dummy_return(x):
      return (f(x + 0.0001) - f(x)) / 0.0001
   return dummy_return

# These make sense, and are numbers
E3(4)
D(E4)(7)
E1 + 4
E2(4, 7)

# These don't make sense
D(E1)
D(E4)
E3 + 4

Hopefully these examples are illuminating.

That's no restriction on the tree system, but an important issue for the rule. Can you provide arguments why I should prefer this notation?

I think the main reason is simply for uniformity -- variables at the leaves, syntax at the inner nodes.

I suppose it makes a difference whether or not you were using f as a variable of the language expressing an unspecified mathematical function... or if you were using f as a meta-variable in the meta-language referring to some unspecified subgraph of the tree?

("meta-" roughly meaning it's talking about the formal language, rather than being part of the formal language)

Then again, uniformity might not matter -- you might lose nothing, or even gain something, by having function variables on the internal nodes.

 

[Gerenuk]

Thanks for the ideas.

Actually I'm going to write it in python, so node names will be the first element of the nested lists anyway. So basically only leaves have a name and the inner nodes are all "eval" :)

First I want to note that functions are effectively vectors...

I think I know how to solve the function and plugged-in-constant problem. Maybe you can tell me what you think of it.

The problem arises since pluggin in a constant is actually a non-trivial action which is beyond algebraic substitution.

So for
$$a=\operatorname{D}x^2$$
$$x=1$$
I would have

  truth
 /    \
 =     =
/ \   /  \
a D   x  1
  |
  sqr
  |
  x

Now substituting the left x with 1 is actually a non-trivial rule which derives from the possibility to replace an expression by anything it is related to by the "=" sign.

So an additional rule for my program should be:
If there is an operator on top, do not allow substitution (i.e. replace expr by smthg it's equal to) if the substitution is not 1-to-1 (so x=a maps 1 to 1 but x=1 doesn't). This is very similar to the rule for change of variables under integrals.