Finite function circuits

Kragen Javier Sitaker, 2017-02-16 (updated 2019-05-17) (29 minutes)

I was considering how to specify finite state machines, and some interesting ideas occurred to me.

This is related to the notation for directed graphs in Graph construction and the algebra of textures in An algebra of textures for interactive composition. (Circuit notation is more concerned with describing the topology of circuit netlists, as you might use for designing analog circuits, while this note is concerned with designing digital circuits, and in particular sequential digital circuits, in terms of finite functions on alphabets; when considering a circuit, this is a higher level of abstraction, though it may well be a lower one when considering some dynamical system you want to simulate with the circuit.)

Introduction and outlook

A synchronous sequential digital circuit is a finite state machine, FSM. At each clock cycle i, it has exactly one state Sᵢ ∈ Σ, and on each transition of the clock, it enters a new state Sᵢ₊₁ ∈ Σ = F(Sᵢ, Iᵢ₊₁), where Iᵢ₊₁ ∈ Υ is its input at the end of clock cycle i, and F ∈ Σ × Υ → Σ is its “state transition function”. In this way, it generates a word in Σ* of letters from Σ from an initial state S₀ and a word in Υ* of letters from Υ.

(This is “circuit” in the sense of an electronic device, not in the theory-of-computation sense of a DAG of combinational logic.)

For example, here’s an execution trace of a finite state machine that transliterates from lowercase Greek into titlecase Roman letters:

Iᵢ:   π λ α τ ο ν ␣ κ α i
      ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓
Sᵢ: ℵ→P→l→a→t→o→n→␣→K→a→i

It should be noted that, since Σ and Υ are finite, so too is Σ × Υ to which the domain of the state transition function F belongs, so it is possible to list F explicitly as an exhaustive case analysis. The state transition function for the above example would include cases like these:

(ℵ, π) → P
(P, π) → p
(P, λ) → λ
(Q, λ) → λ
(ℵ, λ) → Λ
(n, ␣) → ␣
(␣, λ) → Λ
(␣, κ) → K

In this case the input alphabet Υ and the state alphabet Σ are not the same; although they each include a symbol represented as ␣ here, that is just a notational pun — it doesn’t make sense to say that those symbols are the same symbol or that they are different symbols, since they belong to different alphabets.

A full exhaustive case analysis here, supposing that Υ contains the 24 lowercase Greek letters plus ␣, and Σ contains the 26 uppercase modern Latin letters, the corresponding 26 lowercase, ␣, and the initial state S₀ = ℵ, would require 25·54 = 1350 cases. This table is awkward to write out by hand, but it is small enough to be easily manipulated by computer. However, nearly all circuits of interest have far too many possible transitions to fit such a table in the memory of a conventional computer.

In the registers of the circuit we store a Sᵢ, represented as some arrangement of bits; we interpret the set of inputs as Iᵢ₊₁; and we represent the state transition function F as the RTL of our circuit, which can be realized with LUTs, combinational logic made of DAGs of gates (the theory-of-computation meaning of “circuit”), an EPROM, or whatever.

To design the circuit, it is not necessary to list the registers or even Σ — they can be inferred from F and S₀. The representation of Υ can be specified or free for the optimizer to optimize.

Thus we can design a sequential digital synchronous circuit simply by specifying its state transition function. Since that function’s domain is finite, it is possible to do so by enumerating all its cases. However, usually it is preferable to use a more powerful language to be able to compose the desired function from sub-functions that are separately understandable, verifiable, and reusable.

It bears repeating that these are not the “functions” of JS or C, that is, subroutines. Subroutines are executed over some period of time, possibly terminating and possibly crashing. I’m talking about the mathematical object called a function: a mapping from each domain value to exactly one range value.

I will outline here a design for a language for specifying such finite functions that, I think, combines a number of advantages in a way no previous design I’ve seen does.

Design goals

Concision, flexibility, tractability, simulability, synthesizability

A relational algebra

Above, a sequential circuit was described according to its state transition function — its domain being the cartesian product of some finite alphabet of states Σ and some finite alphabet of inputs Υ and its range being Σ — and some assignment of Σ and Υ to concrete bitstrings. To each item in the domain it associates precisely one item in the range. We can generalize this to a state transition relation, in which each item in the domain is associated with any number of items in the range; this describes a potentially nondeterministic circuit, or a design specification with some liberty. A common way for this to occur in real life is for the circuit to have “don’t care” combinations which we expect not to arise in practice. For example, a specification for adding BCD numbers need not specify what happens when the inputs aren't BCD numbers, but some other bit pattern. Also, though, we will see that it’s often convenient to construct a deterministic function out of nondeterministic relations. We can also generalize to binary relations between any alphabets whatsoever.

(Historically, “relation” has meant this kind of binary relation, but since the 1970s a rich theory of N-ary relations has grown up around databases. Here we will completely ignore N-ary relations, being concerned only with binary relations.)

Mostly we will be concerned with finite relations among finite sets, though sometimes they are exponentially large. This means that most of the algorithms we’re interested in are trivial in the sense that at worst they need only enumerate some finite set of cases.

The algebra defined

(Very little of this is original.)

Here’s the definition of the algebra of relations we’ll be using, which is explained in more detail below. Consider a relation as a set of (domain element, range element) pairs; this gives us standard definitions of ∪, ∩, and \ operations, to which we add the following definitions of →, K, ∘, ⁻¹, car, cdr, ×, and *; note in particular that × is not the Cartesian product of sets:

x ∈ a → b⇔x = (a, b)
x ∈ K(b)⇔∃a: x = (a, b)
x ∈ A∘B⇔∃a: ∃b: ∃c: x = (a, c) ∧ (b, c) ∈ A ∧ (a, b) ∈ B
x ∈ A⁻¹⇔∃a: ∃b: x = (a, b) ∧ (b, a) ∈ A
x ∈ car⇔∃a: ∃b: x = ((a, b), a)
x ∈ cdr⇔∃a: ∃b: x = ((a, b), b)
x ∈ A×B⇔∃a: ∃b: ∃c: x = (a, (b, c)) ∧ (a, b) ∈ A ∧ (a, c) ∈ B
x ∈ A*⇔∃i ∈ ℕ: x ∈ A*ᵢ, where
A*₀ = A
i > 0 ⇒ A*ᵢ = A*ᵢ₋₁ ∪ A∘A*ᵢ₋₁

(This is somewhat related to Binate and to the function notation in Pattern matching and finite functions.)

Sometimes people consider the domain and range sets to be part of the content of a relation, aside from its pairs of elements, in the sense that two relations are not equal if they have the same sets of pairs of elements but different domains or ranges (which necessarily in this case include some elements that don’t occur in any of their pairs). Here, however, when we mention the “domain” or “range” of a relation, we mean the sets of elements that occur on the left or right side of its pairs.

XXX typing this fucking Unicode is getting on my fucking nerves. Maybe I should switch to “.” (the other way around) for ∘, “;” for ∪, “:” for →, “~” or “'” or something for ⁻¹, "&" or something for ∩, and some other things?

Constructing relations from items: → and K

The operator → produces a relation consisting of a single pair: a → b is the set {(a, b)}. So, applied to a, this relation gives us {b}, and applied to anything else, it gives us the empty set.

(Originally I was going to use ↦ rather than →, but I have → on my keyboard, and I gave in to expediency.)

The operator K(x) gives us a constant function whose value is x everywhere.

These are the only two operators of our eleven-operator algebra which take elements of relations, rather than relations, as operands. We could consider the tuple-construction operation “(,)” that constructs (u, v) from u and v as an operation on elements, but it doesn’t belong to the algebra proper; we only use it in the meta-notation we’re using to describe the algebra.

Constructing relations with set operations: ∪, ∩, and \

The ∪ set union operator allows us to construct a possibly larger relation from two relations. With ∪ and → we can construct all finite relations simply by listing the cases: (ℵ, π) → P ∪ (P, π) → p ∪ (P, λ) → λ, and so on. If we sort the clauses, we can consider this a canonical form, in the sense that two finite relations will have different canonical forms if and only if they map some domain element to different sets of range values.

The ∩ set intersection operator allows us to construct a possibly smaller relation from two relations, as does the \ set-subtraction operator. So, for example, (α → a ∪ υ → y ∪ υ → u) ∩ (υ → y ∪ υ → v) is just υ → y, and (α → a ∪ υ → y ∪ υ → u) \ (υ → y ∪ υ → v) is (α → a ∪ υ → u).

We could define these in the same style as the above definitions, but it hardly seems necessary, since we’re just using them in the conventional way on sets that happen to be relations:

Call a relation R deterministic if ¬∃x: ∃y: ∃z: (x, y) ∈ R ∧ (x, z) ∈ R ∧ y ≠ z, which is to say that it’s a function, and reversible if correspondingly ¬∃x: ∃y: ∃z: (y, x) ∈ R ∧ (z, x) ∈ R ∧ y ≠ z. (I was going to use “injective” for “reversible”, but apparently sometimes “injective” is used to mean what I mean by “deterministic”.) In particular, the empty relation ∅ is trivially deterministic and reversible.

All three of these operations preserve finiteness; they cannot construct an infinite relation from finite relations. (This is the reason for using \ rather than the more conventional set complement.) Only ∪ preserves infinity, in that the intersection or difference of infinite relations may be finite, but generally we don’t care about preserving infinity.

∩ preserves determinism and reversibility — if either argument is deterministic, the result is deterministic, and similarly for reversibility. Importantly, though, it does not preserve nondeterminism or irreversibility: the intersection of two nondeterministic, irreversible relations may be deterministic and/or reversible. Indeed, it may be empty.

\ preserves determinism and reversibility in its left argument.

∪ does not preserve determinism and reversibility, but it does preserve nondeterminism and irreversibility: if the result is deterministic, both of the operands were deterministic, and similarly for reversibility.

The usual properties of set operations hold in the usual way, with the usual adaptation of DeMorgan’s laws and the distributive and associative laws to set subtraction:

We can also derive some laws for how they combine with the primitive relation constructors:

(All of these, like the other laws presented below, can be proved in terms of the pointwise definition of the operators above.)

Composing relations with ∘

As a generalization of function composition, A∘B maps some element a to some element c precisely when B maps a to some (possibly different) element b, and A then maps that element b to c. So, for example, (1 → 3) ∘ (0 → 1) is (0 → 3). The reversals of direction are most unfortunate, XXX maybe I should switch to using | or . and the other direction of composition.

∘ preserves finiteness in the sense that the composition of two finite relations is also finite. The composition of a finite relation with an infinite one, or vice versa, or the composition of two infinite relations, may be either finite or infinite; but in particular A∘B has B’s domain, or some subset thereof, and A’s range, or some subset thereof, so if B’s domain and A’s range are both finite, then A∘B is finite, even if neither A nor B is finite.

∘ preserves determinism and reversibility in that the composition of two deterministic relations is deterministic, and the composition of two reversible relations is reversible. Nothing in particular can be said about the other combinations.

∘ has a number of useful algebraic properties: XXX some of these are probably wrong

Inverting relations with ⁻¹

A⁻¹ is a relation that interchanges the domain and range of A, a generalization of taking the inverse of a function; so, for example, (p → q ∪ p → r ∪ q → r)⁻¹ = (q → p ∪ r → p ∪ r → q). Unlike the case with functions, every relation has an inverse, which is also a relation, and A⁻¹⁻¹ is always precisely A.

A⁻¹ is finite if A is finite, and it’s reversible if A is deterministic, and conversely deterministic if A is reversible.

We can write down some laws for how ⁻¹ combines with other operators:

From these we can derive an unending farrago of worthless variants like B∘A⁻¹ = (A∘B⁻¹)⁻¹, (a → b ∪ c → d)⁻¹ = b → a ∪ d → c, A∩B∩C = (A⁻¹ ∩ B⁻¹ ∩ C⁻¹)⁻¹, and so on.

Constructing and deconstructing aggregates with car, cdr, and ×

The × “relational product” operator, if applied to two relations A and B over the same domain, produces a new relation A×B with the same domain, but whose range is the Cartesian product of the ranges of A and B — it consists of pairs constructed from an item from A’s range and an item from B’s range. This allows you to take two relations from the same range and combine their results into a single relation. So, for example, (x → y) × (x → z) is x → (y, z).

What × has joined together, the car and cdr relations put asunder; car∘(A×B) is some subset of A, all of A if B didn’t lack any of A’s domain values, and cdr∘(A×B) is analogously some subset of B, all of B if A didn’t lack any of B’s domain values. For example, (y, z) → y ∈ car, while (y, z) → z is in cdr.

car and cdr are unapologetically infinite and polymorphic, even Protean, but they have the property that composing them on the left (car∘R, cdr∘R) with a finite relation R produces another finite relation.

You might complain that car, cdr, and × reintroduce the asymmetry between domain and range that we dispensed with when we moved from functions to more general relations. This is merely a matter of convenience; you can use (A⁻¹×B⁻¹)⁻¹ or R∘car⁻¹ nearly as easily as you can use A×B or car∘R, so there is no need to provide them as separate operations.

× preserves finiteness in the sense that the product of two finite relations is finite, but the product of two infinite relations, or a finite relatin with an infinite relation, may be either finite or infinite. More precisely, if either A or B has a finite domain, A×B will have a finite domain, and if both A and B have finite ranges, A×B will have a finite range. × does not preserve infinity in any of these cases, in the sense that A×B may be finite even if both A and B have infinite domains and infinite ranges.

× preserves determinism in the sense that if A and B are both deterministic, then so is A×B. In this case, A×B will also have no more pairs than either A or B — precisely the same number if and only if they are deterministic and their domains are equal. It preserves reversibility in the stronger sense that if either A or B is reversible, then so is A×B.

× has some interesting algebraic properties:

XXX this is simpler than the kind of relational product I eventually ended up using in Binate, but I imagine I’m going to end up with a bunch of opaque definitions saying things like “carry = car∘car∘cdr” in particular circuits. The Binate approach avoids that, and also sort of avoided the problem of infinities associated with car and cdr. The idea there was that you would write {x: Xexpr, y: Yexpr, z: Zexpr}, and that would be a relation from the (intersected) domains of Xexpr, Yexpr, and Zexpr to records, one for each triple of range elements; then, new field-selection relations x, y, and z related those records to their individual fields. This avoids the problems of infinities and polymorphism mentioned above, but it’s definitely conceptually more complicated, and I think the algebraic laws described above are a lot harder to state in the named-field case. On the other hand, I’m not sure how useful such algebraic identities will really be.

Transitive closure: *

XXX maybe this should be +? Because the * suggests that maybe zero times through the relation is fine too, in which case the identity should be included, and it isn’t. It would also help avoid the semantic collision with Kleene closure once we get to regular expressions.

A* is a superset of A; it’s the smallest relation such that A*∘A = A*. If A tells you where you can get in one move, A* tells you where you can get to in one or more moves. A* = A∪(A∘A)∪(A∘A∘A)∪.... So, for example, (p → q ∪ q → r)* = (p → q ∪ p → r ∪ q → r).

*, surprisingly, preserves finiteness: a finite relation A necessarily has finite domain and finite range, and A* has precisely the same domain and range as A. This provides a convenient way of enumerating A* in finite time for finite relations A, despite its recursive definition.

If A’s domain and range are disjoint, A* = A.

* does not preserve determinism or reversibility, as can be seen by the example above in which the transitive closure of a deterministic, reversible relation is neither deterministic nor reversible. Indeed, I think A* can only be deterministic or reversible if A* = A.

* has relatively few useful algebraic properties:

Regular expressions

Concurrency

Nondeterminism

State trees

Example: XOR from NAND

Example: J-K flip-flop

Example: divide by 2 counter

Example: 3-bit magnitude comparator

Example: ring counter

Example: quadrature decoding

Example: quadrature step counting

Example: bit-serial addition

Example: bit-parallel addition

Example: simple ALU

Example: Single-port RAM

Example: Dual-port RAM

Example: 16-bit multiplier

Notes from the paper notebook

I started writing this file in 2017, and then never finished it; I just found it again now in 2019. But I have some notes from a paper notebook, in Spanish, which I am attempting to transcribe here. I appear to have been working from them when I originally wrote this file.

The expression notation for algebraically composing binary relations is fairly similar to Binate; you have relational composition, transitive closure (which, as a note later in this file points out, is necessarily terminating on finite sets), Cartesian product, union, intersection, set subtraction, relational inverse, relations car and cdr for dissecting Cartesian products, and notations for constant functions and primitive relations consisting of pairs of elements.

It’s not a particularly tiny algebra — it has eleven primitives, of which two are primitive relations, one constructs a relation from an element, one constructs a relation from two elements, two more construct a relation from another relation, and the remaining five construct a relation from two relations. And, implicitly, there’s the tuple-creation operator, which constructs an element of A × B from an element of A and an element of B. But, at least for finite relations — which are all we care about for specifying combinational logic! — it is complete (which really only requires ↦ and ∪) and I think may fulfill the desiderata I laid out below of being concise and flexible, and is certainly tractable, simulable, and synthesizable.

Then I use the union and primitive pairs to build up boolean NOT, and then without mentioning elements again, build up bitwise identity, the universal relation on bits and from pairs of bits to bits, restrictions of car and cdr to relations from pairs of bits to bits (called L₂ and R₂), their bitwise inversions, and finally a relation called NI₂, which I think is (1, 1) → 1 ∪ (0, 0) → 0. I’m pretty sure this is what I was thinking about in the “Example: XOR from NAND” section below: build up all the primitive gates from just a NAND relation (rather than from NOT and AND as I was trying on paper).

I think I was trying to derive AND from just NOT and the primitive relations, so that I would have an algebraic derivation of a whole Boolean algebra from just a definition of NOT. I think doing this isn’t possible, because NOT is symmetric under exchange of 0 and 1, while AND is not. I think it also requires the use of some form of negation, which I hadn’t tried using yet, and although I had included set subtraction in my set of logical definitions of operations, I had omitted it from the list at the end!

My comments about which relations are finite and which are infinite suggest that I was worried about infinite sets popping up and making algorithms fail to terminate, as does my use of set-subtraction \ rather than simple negation, and the aside (on the facing page, which I set aside for asides) about providing only A÷B instead of B⁻¹, which would keep infinite sets that occur in the range confined to the range, preventing them from escaping into the domain and making it infinite too. This would have preserved the ability to finitely enumerate the domain of any relation except car and cdr (which I suggested demoting in the same aside) although if ranges were infinite anyway I'm not sure why that would be especially useful.

I think the idea then was that you can consider a binary relation to be a specification of a combinational logic function, and you can consider that combinational logic function to be a specification of a sequential logic behavior (if you can identify which parts are state and which are inputs, anyway); but, that under other circumstances, other forms of behavior specification, such as the sequence/alternation/repetition operations of regular expressions, are more convenient; and that other ways of combining finite state machines, such as (some unspecified form of) concurrency, (some unspecified form of) nondeterminism, and (some unspecified form of) state trees, are sometimes more useful.

You could conceivably treat an FSM (S₀, F) as a relation from input strings to output strings — a function, if deterministic, but in any case a relation — and attempt to handle them with the same algebra of relations. But I’m not sure I had that in mind, and it may not be a useful way to compose finite state machines. I suspect I just had in mind that you would construct primitive finite state machines using binary relations to specify their transition function, then use the other mechanisms to combine these primitive state machines in series, in parallel (note that tconcurrency was a heading not in the paper notebook), nondeterministically, and in trees of state (perhaps as in Harel statecharts, although I didn’t know about those then).

Componer FSMs

Intro

Un circuito digital sincrónico es una máquina de estados finitos, FSM por sus siglas en inglés. En cada momento tiene un estado Sᵢ ∈ Σ, y en cada transición del reloj entre un nuevo estado Sᵢ₊₁ ∈ Σ = F(Sᵢ, Iᵢ) donde Iᵢ es su entrada en momento i, y F es una función ∈ Σ × Υ → Σ. Así genera una palabra en Σ* a partir de una palabra en Υ* y un estado inicial S₀.

π λ α τ ο ν ␣ κ α i
↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓
P→l→a→t→o→n→␣→K→a→i

Cabe destacar que, ya que Σ y Υ son (ilegible) así también Σ × Υ, así (ilegible) hacer un listado de F.

No incluidos:

En los registros del circuito almacenamos Sᵢ, representando como un conjunto de bits, interpretamos el conjunto de entradas como Iᵢ, y representamos F como el RTL del circuito, que se puede realizar con LUTs, lógica combinacional de DAGs de compuertas (un “circuito” de teoría de computación), un EPROM, lo que sea.

No es necesario especifcar los registros ni Σ — se pueden inferir de F y S₀. La representación de Υ puede ser especificado o libre para optimizar.

Así que podemos diseñar un circuito digital secuencial sincrónico especificando su función de transición nomás, y ya que es finita, lo podemos hacer enumerando los casos. Pero para la mayoría de circuitos, nos conviene usar un lenguaje más poderoso para poder componer la función deseada de sub-funciones separadamente entendibles, verificables, y reutilizables.

Cabe repetir que ésos no son las “funciones” de JS o C, es decir, subrutinas, que pueden ejecutarse y así tomar tiempo.

Relaciones

Así con ↦, K, car, cdr, ⁻¹, ∩, ∪, ×, *, y ∘, podemos combinar relaciones para formar otras relaciones, y podemos construir cualquier relación finita.

(ilegible) va al (intentar?) (evitar?) dominio inf(inito?) es brindar una operacion A ÷ B = A ∘ B⁻¹. Pero no ayuda con car y cdr (pero pueden ser sus propias operaciones.)

De éstas operaciones, car, cdr, y K(x) son relaciones infinitas, y los otros solo general relaciones infinitas a partir de relaciones ya infinitas.

NOT es 1 ↦ 0 ∪ 0 ↦ 1.

AND es (0, 0) ↦ 0 ∪ (0, 1) (ilegible) (1, 0) ↦ 0 (ilegible) a partir de NOT sin ↦.

Topics