What does it mean for symbolic shapes to be equal

One of the first important questions to be answered when composing expressions (such as via binary operators) is whether their shapes match.

What are the semantics of this?

!3 (merged) uses structural equality, but we haven't spelled out whether that's policy.

Other options along a spectrum:

• Structural equality (as symbolic expressions): the strictest
• Structural equality (as symbolic expressions) after algebraic canonicalization: allows for some flexibility
• "Lazy" equality: assume two symbolic shapes are equal unless provable otherwise (perhaps via isl-style assumptions): the least strict

Another aspect of structural equality: two names in the namespace could refer to the same node in the graph. So, shape equality might have to take into account graph node equality.

This has implications for broadcasting too. If/when we implement broadcasting, how hard do we check that the dimension has length 1?

One implication of structural-only policy is that, length 1 can only be identified if it is set to integer 1. Because 2 // 2 and 1 are structurally different.

Agreed.

>>> parse("2//2") == 1
False

mentioned in merge request !3 (merged)

My vote is structural-only.

@xywei Thoughts?

I am for structural-only as well, just because of its simplicity.

Here are some extra thoughts:

As a future step, I can see the benefits of allowing more flexible shape constraints.

Alternative to "lazy equality", we could attach to each namespace a "knowledge base" of constrains. On node construction, the operator makes queries to see if its input constraints are satisfiable, and update the knowledge base accordingly. On execution, the loopy kernel wrapper can also make queries to see if the actual input shapes satisfy the constraints.

I am proposing the knowledge base approach because there are existing predicate logic tools like Prolog that can be leveraged. Specifically, the CLP(FD) capability (short for "Constraint Logic Programming over Finite Domains") handles constraint propagation and unification, which are the most algorithmically-challenging parts to implement.

Here is a conceptual example of using Prolog to manage constraints carried out in swipl. For simplicity, I put all constraints inside one sentence. ?- is the command prompt, and the lines below it are command outputs. If a command outputs true. or a solution, we say that Prolog thinks that the constraints are satisfiable:

• Import CLP(FD) module

  ?- use_module(library(clpfd)).
  true.

• Say we start with an array of shape (m, n). (Prolog variable names start with _).

  ?- _m #>= 1, _n #>= 1.
  _m in 1..sup,
  _n in 1..sup.

  In Prolog, >= does structural comparison, and #>= does arithmetic comparison.

• The array is reshaped into (k, k).

  ?-_m #>= 1, _n #>= 1, _m * _n #= _k * _k, _k #>= 1.
  _m in 1..sup,
  _m*_n#=_22220,
  _n in 1..sup,
  _22220 in 1..sup,
  _k^2#=_22220,
  _k in 1..sup.

  Unlike isl, CLP can take nonlinear expressions. Also, we cannot expect it to solve any nonlinear algebraic equation, so it may give "false negatives" like:

  ?- (_m + 1)^2 * (_m + 3)^2 #= 0, _m #> 0.
  _m in 1..sup,
  _m+3#=_8420,
  _m+1#=_8444,
  _8420 in 4..sup,
  _8420^2#=_8492,
  _8492 in 16..sup,
  _8544*_8492#=0,
  _8544 in 4..sup,
  _8444^2#=_8544,
  _8444 in 2..sup.

• At compile time, to generate code, we have to fix two of {m, n, k}. Fixing m and n. This also gets rid of false negatives:

  ?-_?- _m #>= 1, _n #>= 1, _m * _n #= _k * _k, _k #>= 1, _m = 10, _n = 40.
  _m = 10,
  _n = 40,
  _k = 20.

  Fixing n and k:

  ?- _m #>= 1, _n #>= 1, _m * _n #= _k * _k, _k #>= 1, _m = 10, _k = 20.
  _m = 10,
  _n = 40,
  _k = 20.

  If invalid values are encountered:

  ?- _m #>= 1, _n #>= 1, _m * _n #= _k * _k, _k #>= 1, _m = 10, _n = 12.
  false.

IMO, this could be a future extension once pyswip matures.

That might make for an interesting extension. I think SMT solvers cover roughly the same problem space, and they seem to have Python libraries too.

mentioned in commit b1d614b0