Proper implementation of 2D expressions

[wwitzel]

New idea for implementation of ExprTensor is to have items on a uniform grid. Joining rectangular regions would be done via style, keeping the internal representation simple. Perhaps it should be called ExprGrid instead of ExprTensor.

[wwitzel]

Start with the "join" functionality for the 1D case. For example, A{1}, ..., A{m}, A{m+1} should automatically merge into A{1}, ..., A{m+1}. Also, A{1}, ..., A{m}, A{m+1}, ..., A{n} should merge into A{1}, ..., A_{n} but must require that n>=m.

[wwitzel]

E-mail from Feb. 16 2019 from Wayne to Deepak (and cc'ing Bob, Steven, and Jon). Subject: 2D expression representations, simplified

Hi Deepak,

I think we had a valuable conversation yesterday, especially after you came back from interviewing your candidate and we discussed things a little more. i think I have a nice plan now, inspired by our discussion. It's simple and clean. Here's the basic idea:

ExprList: a list of items. Each item is either a singular element or an iteration (that may be parameterized). ExprTensor: a regular grid of items. Each item is either singular element or an iteration. Iterations represent blocks with parameterized dimensions. The blocks must line up.

At first glance, this seems less flexible than what we wanted. You aren't able to intrinsically have rectangular regions that are misaligned with respect to each other. For example, it seems that you can't do something like: A_1 B_1 B_2 A_2 C_1 D_1 where A_1, A_2 should be considered one block that's a vertical rectangle and B_1, B_2 should be considered one block that's a horizontal rectangle. But the way I've expressed it here gives the hint for how we can effectively represent this using a regular grid. Each block is an iteration. An iteration is a lambda map with start indices and end indices. Therefore A_1 should really represent something like:

A{1,1} ... A{1,m} . . . . . . A{n,1} ... A{n,m}

and A_2 could be:

A{n+1,1} ... A{n+1,m} . . . . . . A{n+k,1} ... A{n+k,m}

or whatever. The point is, it is easy to tell from the form of these iterations, having the same lambda map and having indices with the proper alignment, that they can be merged together in one rectangular iteration:

A{1,1} ... A{1,m} . . . . . . A{n+k,1} ... A{n+k,m}

So, we can do the following. Internally, we can use the regular grid representation where A_1 and A_2 are separate items in the grid. However, when the representation is formatted for display, it is a style matter and we can choose to display the A_1, A_2 pair as a single block going from (1,1) to (n+k,m).

This should be relatively simple to implement. Indexing into this grid structure will be simple. Substitution will be more of a challenge, but should not be too bad. We just need to deal with the possibility that the grid may need to be broken up along an axis and/or possibly fuse along an axis. To see that fusing is a possibility, consider replacing D_1 in the above example with C_2. Then we'd have

A_1 B_1 B_2 A_2 C_1 C_2

which should merge, for a unique representation, into

A_1 B A_2 C

We should handle mergers in the 1D version in the same manner.

I'm happy with this. I think this is the way to go. I am thinking of renaming ExprTensor to ExprGrid, however.

[wwitzel]

Excerpted from another e-mail sent 6/13/2019 following up with quantum circuit representations:

... I said that we also had an "A-Ha!" moment to the contents of the copied e-mail below but regarding quantum circuit equivalences, in particular. I'm going to do may best to recall, but I haven't been able to find anything written down about this. I remember discussing it on the whiteboard with Deepak and others. Maybe they have notes, but I'll do my best to recall the main ideas.

The basic idea was to represent a quantum circuit as an ExprArray as described in the below e-mail. As is convention, the rows are different qubits and the columns are sequential in time. Each element of the array represents a gate operation that may involve one or more qubits -- the one corresponding to its row, but potentially other qubits as well if it is a multi-qubit gate. A key insight is to identify qubits in absolute terms with respect to row indices, rather than relative terms. Also, a multi-qubit gate will be encoded redundantly across each of the rows involved. For example, consider a CNOT gate between qubit 1 and 2 at time 5. This might have something like ZX(1, 2) at row 1 column 5 and ZX(1, 2) at row 2 column 5. A reason for identifying the qubits in absolute terms instead of relative terms is that it will be convenient to apply a rule (theorem) stating that a quantum circuit equivalence is preserved under the permutation of qubit indices (rows). (That's it! It's coming back to me. Phew!) If circuitA is equivalent (performs the same transformation as) circuitB, then circuitA under qubit permutation pi is equivalent to circuitB under the same qubit permutation pi. To perform this permutation transformation, you permute the rows and all of the qubit indices used in quantum gates. In the above example, if we switch qubit 1 and 2, we would end up with: ZX(2, 1) at row 1 column 5 and ZX(2, 1) at row 2 column 5.

We would also have various composition rules. We could combine two quantum circuit equivalences in parallel (running them at the same time on different blocks of qubits) if they have the same number of columns, or in series (running one after the other) if the have the same number of rows. As an example of the latter, if circuit A is equivalent to circuit B and circuit C is equivalent to circuit D and they all have the same number of rows, then circuit A followed by B is equivalent to circuit C followed by D. Using such composition rules and permutations, we should be able to "apply" quantum circuit equivalences to transform circuits in any context.

I think these were the basic ideas and may evolve somewhat as things develop. Let me know whether or not this makes sense. I'm just glad to get this written down somewhere finally.

[wwitzel]

Re-thinking about iteration substitution algorithm, replacing previous arbitrary ExprTensor concept with more structured ExprGrid concept:

Obtain simplified "entry coordinates" coming from each contained expanded inner indexed variable, making proper translations to account for indexing parameterization. Each one is in sorted order, but we need to collate them together (merge sort) to determine how to break up the result (important for ExprGrid or in 1D cases as well when parameterizations change: e.g., xi * y{i+1}). When do we need to make sure that ranges have an extent that is a natural number? When could we obtain a contradiction because this is violated? When an Iter is constructed, we do not want to bother checking that it is a proper range (for logistic reasons -- expressions should not have intrinsic requirements, see issue #37). But, when an iterated indexed variable is replaced with something concrete, for example, we need to make sure that this is the proper realization of the iteration by ensuring that the end-start+1 is a natural number. Perhaps the right thing is to make sure that anything that is eliminated off of the ends (e.g., windowing a region within a larger ExprTuple or ExprGrid) that those are all kosher, because we won't be able to verify that stuff later since it is being eliminated. For the inside stuff, however, we could perhaps avoid worrying about until necessary.

[wwitzel]

One recent realization regarding iterations, in order for their expansions to be unambiguous and sensibly defined, Iter expressions must only contain Indexed variables with indices that are 'simple' functions of an iteration (the parameter itself or a sum of terms with one term as the parameter).

For example, you can have x_1, ..., xn and you can have x{1+k}, ..., x{n+k} or x{k+1}, ..., x{k+n} but not x{1^2}, ..., x{n^2} or x{21}, ..., x_{2n}.

[wwitzel]

Here is something I am struggling with a bit as I'm working on a proper implementation for expanding iterations (independent of 1-D or 2-D). When an iteration gets expanded, we generally need to break up the ranges of the iteration parameter. For example a_1b_1 + ... + a_nb_n when substituted with a:(x_1, ..., x_j, y_1, ..., y_k) b:(z_1, ..., z_k, x_1, ..., x_j) under the assumption that j<k will be transformed into x_1z_1 + ... + x_jz_j + y1*z{j+1} + ... + y{k-j}*z{j+(k-j)} + y_{k-j+1}x1 + ... + y{k-j+j}x_j So you see here we needed to break up the 1...j+k range into 1...j, (j+1)...k, (k+1)...*(j+k). But we have to be careful with the ranges because it is possible to have an empty range (e.g., j could be zero or k could be zero). So if we list the endpoints of all of these ranges (1, j, j+1, k, k+1, j+k), we cannot assume they are in sorted order. Instead, we can use the start of each range and one plus the last endpoint and they will be properly sorted: 1 <= j+1 <= k+1 <= j+k+1.

But, adding one to the end can be a little annoying for the easier cases. For example, consider the proof of foldInBool: https://pyproveit.github.io/Prove-It//packages/proveit/logic/boolean/_proofs_/foldInBool.html The current proof has the requirement that 1+1=2. But, sorting out the iteration expansion ranges to go 1 past the end would take us out to 3 and require 2+1=3. That should not really be a requirement in the foldInBool proof, but it is kind of important to go one past the end in the example above (if j=k=0, then j+k=0 and is less than 1). Anyway, in working on implementing these things, I've found it is a little tricky to get it right and have no more than the desired requirements. I was using the "exclusive end" strategy (going one past the end) then trying the "inclusive end" strategy when I noticed the foldInBool issue, but now I am back to seeing the need for using the "exclusive end" in certain instances while avoiding the foldInBool issue. That is still in progress.

[wwitzel]

Last week, Deepak showed his way of doing the following example (for expanding a 1D iteration):

a_1*b_1 + ... + a_n*b_n
when substituted with 
a:(x_1, ..., x_j, y_1, ..., y_k)
b:(z_1, ..., z_k, x_1, ..., x_j)
under the assumption that j<k will be transformed into
x_1*z_1 + ... + x_j*z_j +
y_1*z_{j+1} + ... + y_{k-j}*z_{j+(k-j)} +
y_{k-j+1}*x_1 + ... + y_{k-j+j}*x_j

In his version, he emphasized equating the original and split versions of x_1, .., x_j, y_1, ..., y_k as well as z_1, ..., z_k, x_1, ..., x_j. My current implementation does not explicitly show this step. It occurred to me after seeing Deepak's version that I should change the requirements for the iteration so that it requires these equalities of original and split iterations rather than breaking it down (as I do now) into differences being in the set of Naturals and simplification equalities. That would resolve some of my concern that the derivation steps use too much intrinsic knowledge about Naturals and make the proof present better. The algorithm could stay the same essentially, it is just a matter of changing what are the "requirements" for the derivation step.

[wwitzel]

Handled with significant-core-updates merger.