A Denotational Semantics for Constraints

This note gives a denotational semantics for GoFish's layout constraints, in the style of Spytial's Table 1 (Prasad et al., Patterns for Spatial Reasoning): each construct is given a meaning $[[\cdot ]]$ as a mathematical object, independent of how the engine computes it. It is the formal companion to layout-synthesis (the two-semiring engine) and constraints-as-core (the feasibility argument). Where those essays argue that operators reduce to constraints, this one says precisely what a constraint means.

The payoff of writing it down: the meaning of a layer is the composition of its constraints' denotations, and because each denotation lives in a semiring closed under composition, the composite is always well-defined and invertible. That is the completeness conjecture of layout-synthesis, stated semantically.

Semantic domains

A layout assigns every node $n$, on each axis $d\in \{x,y\}$, two quantities:

• an extent $e_d(n)\ge 0$ — its size;
• a position $p_d(n)$ — where its origin sits.

Neither is a free number. Extents are claims: monotone functions of a scale factor $\sigma$ (pixels per data unit), drawn from the carrier

$$\mathsf{Claim}=\{f:{\mathbb{R}}_{\ge 0}\to {\mathbb{R}}_{\ge 0}\mid f\text{ monotone}\}.$$

A fixed box denotes the constant claim $\lambda \sigma .c$; a data value $v$ denotes $\lambda \sigma .v\sigma$; spacing and padding denote constant offsets. Positions, once $\sigma$ is known, are plain reals related by difference constraints $p_d(b)-p_d(a)=w$.

So the meaning of a node splits in two, matching the two passes:

$$[[n]]=([[n]{]}_d^{\mathsf{size}}:\mathsf{Claim},[[n]{]}_d^{\mathsf{pos}}:\text{a set of difference constraints}).$$

The two semirings

Composition happens in two tropical semirings, one per quantity (see layout-synthesis Part 2):

• Sizes compose in $(max,+)$ over $\mathsf{Claim}$: series (stacking) is $+$, overlay (alignment) is $max$, constants are $+c$, data is $\cdot \sigma$. Closed under composition, so any network folds to a single $\mathsf{Claim}$ — hence invertible.
• Positions compose in $(min,+)$: a system of difference constraints is a shortest-path problem; on a forest (one anchor, no alternative paths) the positions are just path sums from the anchor.

$[[\cdot ]{]}^{\mathsf{size}}$ denotes into the first; $[[\cdot ]{]}^{\mathsf{pos}}$ into the second.

The layer is the solver

A constraint is meaningless in isolation — it denotes a contribution to its enclosing layer $L$. The layer composes its children's claims under its constraints' size-folds into one claim per axis, $[[L]{]}_d^{\mathsf{size}}$, then — given an allotted budget $B_d$ — solves the single unknown

$${\sigma }_d=([[L]{]}_d^{\mathsf{size}}{)}^{-1}(B_d)$$

and evaluates: every node's extent is $e_d(n)=[[n]{]}_d^{\mathsf{size}}({\sigma }_d)$. With $\sigma$ fixed, the difference constraints $[[\cdot ]{]}^{\mathsf{pos}}$ become concrete and positions are read off by propagation. (This inversion is exactly Monotonic.inverse; the monotonic module is the implementation of $\mathsf{Claim}$.)

The denotations

Below, a constraint relates a layer's ordered children $c_1\dots c_k$. Write $e_d(c)$ for $[[c]{]}_d^{\mathsf{size}}$ (the child's own claim) and ${\mathrm{anchor}}_a(c,\beta )$ for the predicate "$c$'s chosen anchor on axis $a$ sits at $\beta$" — start: $p_a(c)=\beta$; end: $p_a(c)+e_a(c)=\beta$; middle: $p_a(c)+e_a(c)/2=\beta$; baseline: $c$'s origin $=\beta$. $s$ is spacing, $p$ padding, $\overline{d}$ the cross axis.

distribute (series on axis $d$)

$$[[{\mathsf{distribute}}_d]{]}_d^{\mathsf{size}}=\sum _{i=1}^k{e}_d(c_i)+s(k-1),[[\cdot ]{]}_{\overline{d}}^{\mathsf{size}}=\text{(no contribution)}$$$$[[{\mathsf{distribute}}_d]{]}^{\mathsf{pos}}=\{p_d(c_{i+1})-p_d(c_i)=e_d(c_i)+s{\}}_{i=1}^{k-1}$$

A series: claims add (plus the spacing constant), and positions are a chain of difference constraints — the running-sum walk.

align (overlay on axis $a$)

$$[[{\mathsf{align}}_a]{]}_a^{\mathsf{size}}=\underset{i}{max}{e}_a(c_i),[[{\mathsf{align}}_a]{]}^{\mathsf{pos}}=\{{\mathrm{anchor}}_a(c_i,\beta ){\}}_{i=1}^k$$

for a single shared baseline $\beta$ (taken from the first pre-placed child, else the axis fallback). Overlay: the extent is the $max$; positions collapse all children onto one anchor line.

position (a pin)

$$[[\mathsf{position}(v)]{]}_d^{\mathsf{size}}=\text{datum domain }\{v\}(\text{not an extent}),[[\mathsf{position}(v)]{]}^{\mathsf{pos}}=\{p_d(c)={\mathrm{scale}}_d(v)\}$$

A literal pins to a pixel; a datum $v$ pins through the axis scale. It is the boundary case that seeds a difference-constraint forest with an absolute anchor.

nest (unary, padding $p$)

$$[[\mathsf{nest}(o,i)]{]}_d^{\mathsf{size}}=e_d(o)=e_d(i)+2p(\text{inside-out})\text{or}{e}_d(i)=e_d(o)-2p(\text{outside-in})$$$$[[\mathsf{nest}(o,i)]{]}^{\mathsf{pos}}=\{{\mathrm{center}}_d(i)={\mathrm{center}}_d(o)\}$$

A unary $+\text{constant}$ on the size side; concentric centering on the position side. Which variable is derived is discovered by which one is already determined (the firing rule of layout-synthesis Part 3), not fixed by the operator.

grid (the symmetric 2-D layout)

For cells $c_{r,\gamma }$ in $R$ rows $\times$ $C$ columns (constraints/grid.ts):

$$[[\mathsf{grid}]{]}_x^{\mathsf{size}}=\sum _{\gamma =1}^C(\underset{r}{max}{e}_x(c_{r,\gamma }))+s_x(C-1),[[\mathsf{grid}]{]}_y^{\mathsf{size}}=\sum _{r=1}^R(\underset{\gamma }{max}{e}_y(c_{r,\gamma }))+s_y(R-1)$$$$[[\mathsf{grid}]{]}^{\mathsf{pos}}=\{{\mathrm{center}}_x(c_{r,\gamma })=\gamma (w+s_x)+\frac{w}{2},{\mathrm{center}}_y(c_{r,\gamma })=r(h+s_y)+\frac{h}{2}\}$$

This is the $\mathrm{\Sigma }$-of-max form: a track is the $max$ (overlay) of its cells, and the axis is the $\sum$ (series) of its tracks — $(max,+)$ on both axes, symmetrically. It is exactly two cross-cutting overlay-then-series folds; that the two share the cells (a cell is in one column and one row) is the irreducible 2-D structure the grid constraint owns. The axes additionally denote $\mathrm{ORDINAL}(\text{colKeys})$ / $\mathrm{ORDINAL}(\text{rowKeys})$ for guide rendering.

v1 note. The implementation specializes the equal-track case: every cell fills its track, so $\underset{r}{max}{e}_x=w$ and the equation collapses to $W=Cw+s_x(C-1)$, solved by box-division (sliceExtent). The general $\mathrm{\Sigma }$-of-max (content-sized tracks) and the symbolic flex claim — so this prints as $C\sigma +s_x(C-1)$ — arrive with flex-as-datum (the spread fill story).

overlay (a bare layer) and z-order

A layer with no size-folding constraint denotes pure overlay:

$$[[\mathsf{layer}]{]}_d^{\mathsf{size}}=\underset{i}{max}{e}_d(c_i).$$

zAbove / zBelow denote only a paint order — a relation $\pi (a)>\pi (b)$ on the render sequence, with no size or position contribution. They are the one constraint outside the geometric semirings.

Table 1: the constraints at a glance

constraint	size denotation $[[\cdot ]{]}^{\mathsf{size}}$ — $(max,+)$	placement denotation $[[\cdot ]{]}^{\mathsf{pos}}$ — $(min,+)$	role
distribute	$\sum _i{e}_i+s(k-1)$ on $d$	$p_d(c_{i+1})-p_d(c_i)=e_d(c_i)+s$	series
align	$\underset{i}{max}{e}_i$ on $a$	${\mathrm{anchor}}_a(c_i)=\beta$ (shared)	overlay
position(v)	datum domain $\{v\}$	$p_d(c)={\mathrm{scale}}_d(v)$	anchor / pin
nest(o,i)	$e(o)=e(i)+2p$	$\mathrm{center}(i)=\mathrm{center}(o)$	unary $\pm$ const
grid	$\sum _{\text{tracks}}(\underset{\text{cells}}{max}e)+s(n-1)$, both axes	cell centered in its $(\text{col},\text{row})$ track	symmetric 2-D
layer (bare)	$\underset{i}{max}{e}_i$	children at own positions	overlay
zAbove/zBelow	—	— (paint order $\pi (a)>\pi (b)$)	z-order

Why the composition is total

Read the table column-wise. Every size denotation is built from $+$, $max$, $\cdot \sigma$, and $+c$ — the generators of $(max,+)$ over $\mathsf{Claim}$. $\mathsf{Claim}$ is closed under all four and monotone throughout, so the fold of any set of these over a layer is again a single monotone $\mathsf{Claim}$; it has a (one-unknown) inverse; the budget solve always succeeds. Every placement denotation is a set of difference constraints; over a forest of anchors they have a unique solution by path-sum.

That is the completeness statement of constraints-as-core made precise:

The denotation of a layer of $\{\mathsf{distribute},\mathsf{align},\mathsf{position},\mathsf{nest},\mathsf{grid}\}$ over children with monotone claims is a $(max,+)$ claim on the size side and a difference-constraint forest on the position side — hence always solvable, and closed under nesting.

Operators are then just notations for particular denotations: $\mathsf{spread}=\mathsf{align}+\mathsf{distribute}$, $\mathsf{stack}=\mathsf{distribute}$ (glue), $\mathsf{table}=\mathsf{grid}$. Two constructs sit outside the generators but inside the language (per layout-synthesis): z-order (a render-order relation, no geometry) and custom algorithmic layouts like treemap (arbitrary computation that emits claims, pins, and placements under the same denotations).