Understanding Logic Programming Engines

A simple, practical introduction for developers

When we write programs, we usually describe how to compute something:

do this, then do that, handle these cases, return a result.

Logic programming flips that upside down.

Instead of giving a step-by-step procedure, you describe what is true, and a logic programming …

Committing to matrices with one-hot rows

public lookup table

\(T \in \mathbb{F}^{m \times m}\)

\(T=\begin{bmatrix}1&0&0&…\\0&1&0&…\\0&0&1&…\\…&…&…&…\end{bmatrix}\)

the table to be looked up

\(M \in \mathbb{F}^{n \times m}\), the goal is to prove each row of \(M\) belongs to the rows of \(T\)

for example, \(M\) is as blow (to make it more intuitive to look at)

\(M=\begin{bmatrix}0&0&1&…\\1&0&0&…\\0&0&1&…\\…&…&…&…\end{bmatrix}\)…

Twist – 1

  • \(T\): number of reads in read-only case. number of alternating reads and writes in the read/write case.
  • values returned by any read operation -\(\widetilde{\mathsf{rv}}\)
  • value of register \(k\), \(\mathsf{Val}(k)\)
  • \(\mathsf{ra}(k,j)=\left\{ \begin{aligned} & 1, \quad \text{register} \quad \mathsf{k} \quad \text{is read at cycle} \quad j \\ & 0, \quad \text{otherwise}
…