Tag Archives: math

PenroseKiteDart Animations

About PenroseKiteDart

Below we present some animations that illustrate operations on finite patches of Penrose’s Kite and Dart tiles.

These were created using PenroseKiteDart which is a Haskell package available on Hackage making use of the Haskell Diagrams package. For details, see the PenroseKiteDart user guide.

Penrose’s Kite and Dart tiles can produce infinite aperiodic tilings of the plane. There are legal tiling rules to ensure aperiodicity, but these rules do not guarantee that a finite tiling will not get stuck. A legal finite tiling which can be continued to cover the whole plane is called a correct tiling. The rest, which are doomed to get stuck, are called incorrect tilings. (More details can be found in the links at the end of this blog.)

Decomposition Animations

The function decompose is a total operation which is guaranteed to preserve the correctness of a finite tiling represented as a tile graph (or Tgraph). Let us start with a particular Tgraph called sunGraph which is defined in PenroseKiteDart and consists of 5 kites arranged with a common origin vertex. It is drawn using default style in figure 1 on the left. On the right of figure 1 it is drawn with both vertex labels and dotted lines for half-tile join edges.

We can decompose sunGraph three times by selecting index 3 of the infinite list of its decompositions.

    sunD3 :: Tgraph
    sunD3 = decompositions sunGraph !! 3

where we have used

    decompose :: Tgraph -> Tgraph
    
    decompositions :: Tgraph -> [Tgraph]
    decompositions = iterate decompose

The result (sunD3) is drawn in figure 2 (scaled up).

The animation in figure 3 illustrates two further decompositions of sunD3 in two stages.

Figure 4 also illustrates two decompositions, this time starting from forcedKingD.

    forcedKingD :: Tgraph
    forcedKingD = force (decompose kingGraph)

Figure 4: Two decompositions of `forcedKingD`

A Composition Animation

An inverse to decomposing (namely composing) has some extra intricacies. In the literature (see for example 1 and 2) versions of the following method are frequently described.

Firstly, split darts in half.
Secondly, glue all the short edges of the half-darts where they meet a kite (simultaneously). This will form larger scale complete darts and larger scale half kites.
Finally join the halves of the larger scale kites.

This works for infinite tilings, but we showed in Graphs,Kites and Darts and Theorems that this method is unsound for finite tilings. There is the trivial problem that a half-dart may not have a complete kite on its short edge. Worse still, the second step can convert a correct finite tiling into an incorrect larger scale tiling. An example of this is given in Graphs, Kites and Darts and Theorems where we also described our own safe method of composing (never producing an incorrect Tgraph when given a correct Tgraph). This composition can leave some boundary half-tiles out of the composition (called remainder half-tiles).

The animation in figure 5 shows such a composition where the remainder half-tiles are indicated with lime green edges.

In general, compose is a partial operation as the resulting half-tiles can break some requirements for Tgraphs (namely, connectedness and no crossing boundaries). However we have shown that it is a total function on forced Tgraphs. (Forcing is discussed next.)

Forcing Animations

The process of forcing a Tgraph adds half-tiles on the boundary where only one legal choice is possible. This continues until either there are no more forced additions possible, or a clash is found showing that the tiling is incorrect. In the latter case it must follow that the initial tiling before forcing was already an incorrect tiling.

The process of forcing is animated in figure 6, starting with a 5 times decomposed kite and in figure 7 with a 5 times decomposed dart.

It is natural to wonder what forcing will do with cut-down (but still correct) Tgraphs. For example, taking just the boundary faces from the final Tgraph shown in the previous animation forms a valid Tgraph (boundaryExample) shown in figure 8.

    boundaryExample :: Tgraph
    boundaryExample = runTry $ tryBoundaryFaceGraph $ force $ decompositions dartGraph !!5

Figure 8: boundaryExample — Figure 8: `boundaryExample`

Applying force to boundaryExample just fills in the hole to recreate force (decompositions dartGraph !!5) modulo vertex numbering. To make it more interesting we tried removing further half-tiles from boundaryExample to make a small gap. Forcing this also completes the filling in of the boundary half-tiles to recreate force (decompositions dartGraph !!5). However, we can see that this filling in is constrianed to preserve the required Tgraph property of no crossing boundaries which prevents the tiling closing round a hole.

This is illustrated in the animation shown in figure 9.

As another experiment, we take the boundary faces of a (five times decomposed but not forced) star. When forced this fills in the star and also expands outwards, as illustrated in figure 10.

Figure 10: Star boundary

In the final example, we pick out a shape within a correct Tgraph (ensuring the chosen half-tiles form a valid Tgraph) then animate the force process and then run the animation in both directions (by adding a copy of the frames in reverse order).

The result is shown in figure 11.

Creating Animations

Animations as gif files can be produced by the Haskell Diagrams package using the rasterific back end.

The main module should import both Diagrams.Prelude and Diagrams.Backend.Rasterific.CmdLine. This will expose the type B standing for the imported backend, and diagrams then have type Diagram B.

An animation should have type [(Diagram B, Int)] and consist of a list of frames for the animation, each paired with an integer delay (in one-hundredths of a second).

The animation can then be passed to mainWith.

module Main (main) where
    
import Diagrams.Prelude
import Diagrams.Backend.Rasterific.CmdLine

...

fig::[(Diagram B,Int)]
fig = myExampleAnimation

main :: IO ()
main = mainWith fig

If main is then compiled and run (e.g. with parameters -w 700 -o test.gif) it will produce an output file (test.gif with width 700).

Crossfade tool

The decompose and compose animations were defined using crossfade.

crossfade :: Int -> Diagram B -> Diagram B -> [Diagram B]
crossfade n d1 d2 = map blending ratios 
  where
    blending r = opacity (1-r) d1 <> opacity r d2
    ratios = map ((/ fromIntegral n) . fromIntegral) [0..n]

Thus crossfade n d1 d2 produces n+1 frames, each with d1 overlaid on d2 but with varying opacities (decreasing for d1 and increasing for d2).

Adding the same pause (say 10 hundreths of a second) to every frame can be done by applying map (,10) and this will produce an animation.

Force animation tool

To create force animations it was useful to create a tool to produce frames with stages of forcing.

forceFrames :: Angle Double 
            -> Int
            -> Tgraph 
            -> (Colour Double, Colour Double, Colour Double)
            -> [Diagram B]

This takes as arguments

an angle argument (to rotate the diagrams in the animation from the default alignment of the Tgraph),
an Int (for the required number of frames),
a Tgraph (to be forced),
a triple of colours for filling darts, kites and grout (edge colour), respectively.

The definition of forceFrames uses stepForce to advance forcing a given number of steps to get the intermediate Tgraphs. The total number of forcing steps will be the number of faces (half-tiles) in the final force g less the number of faces in the initial g. All the Tgraphs are drawn (using colourDKG) but the resulting diagrams must all be aligned properly. The alignment can be achieved by creating a VPatch (vertex patch) from the final Tgraph which is then rotated. All the Tgraphs can then be drawn using sub vertex patches of the final rotated one. (For details see Overlaid examples in the PenroseKiteDart user guide.)

PenroseKiteDart user guide – this explains how to install and use the PenroseKiteDart package.
Graphs,Kites and Darts and Theorems established some important results relating force, compose, decompose.
Empires and SuperForce – these new operations were based on observing properties of boundaries of forced Tgraphs.
Graphs, Kites and Darts introduced Tgraphs. This gave more details of implementation and results of early explorations. (The class Forcible was introduced subsequently).
Diagrams for Penrose Tiles – the first blog introduced drawing Pieces and Patches (without using Tgraphs) and provided a version of decomposing for Patches (decompPatch).

References

[1] Martin Gardner (1977) MATHEMATICAL GAMES. Scientific American, 236(1), (pages 110 to 121). http://www.jstor.org/stable/24953856

[2] Grünbaum B., Shephard G.C. (1987) Tilings and Patterns. W. H. Freeman and Company, New York. ISBN 0-7167-1193-1 (Hardback) (pages 540 to 542).

Graphs, Kites and Darts – and Theorems

2 Replies

We continue our exploration of properties of Penrose’s aperiodic tilings with kites and darts using Haskell and Haskell Diagrams.

In this blog we discuss some interesting properties we have discovered concerning the $\small\texttt{decompose}$ , $\small\texttt{compose}$ , and $\small\texttt{force}$ operations along with some proofs.

Index

Quick Recap (including operations $\small\texttt{compose}$ , $\small\texttt{force}$ , $\small\texttt{decompose}$ on Tgraphs)
Composition Problems and a Compose Force Theorem (composition is not a simple inverse to decomposition)
Perfect Composition Theorem (establishing relationships between $\small\texttt{compose}$ , $\small\texttt{force}$ , $\small\texttt{decompose}$ )
Multiple Compositions (extending the Compose Force theorem for multiple compositions)
Proof of the Compose Force Theorem (showing $\small\texttt{compose}$ is total on forced Tgraphs)

1. Quick Recap

Haskell diagrams allowed us to render finite patches of tiles easily as discussed in Diagrams for Penrose tiles. Following a suggestion of Stephen Huggett, we found that the description and manipulation of such tilings is greatly enhanced by using planar graphs. In Graphs, Kites and Darts we introduced a specialised planar graph representation for finite tilings of kites and darts which we called Tgraphs (tile graphs). These enabled us to implement operations that use neighbouring tile information and in particular operations $\small\texttt{decompose}$ , $\small\texttt{compose}$ , and $\small\texttt{force}$ .

For ease of reference, we reproduce the half-tiles we are working with here.

Figure 1 shows the right-dart (RD), left-dart (LD), left-kite (LK) and right-kite (RK) half-tiles. Each has a join edge (shown dotted) and a short edge and a long edge. The origin vertex is shown red in each case. The vertex at the opposite end of the join edge from the origin we call the opp vertex, and the remaining vertex we call the wing vertex.

If the short edges have unit length then the long edges have length $\phi$ (the golden ratio) and all angles are multiples of $36^{\circ}$ (a tenth turn) with kite halves having two 2s and a 1, and dart halves having a 3 and two 1s. This geometry of the tiles is abstracted away from at the graph representation level but used when checking validity of tile additions and by the drawing functions.

There are rules for how the tiles can be put together to make a legal tiling (see e.g. Diagrams for Penrose tiles). We defined a Tgraph (in Graphs, Kites and Darts) as a list of such half-tiles which are constrained to form a legal tiling but must also be connected with no crossing boundaries (see below).

As a simple example consider kingGraph (2 kites and 3 darts round a king vertex). We represent each half-tile as a TileFace with three vertex numbers, then apply makeTgraph to the list of ten Tilefaces. The function makeTgraph :: [TileFace] -> Tgraph performs the necessary checks to ensure the result is a valid Tgraph.

kingGraph :: Tgraph
kingGraph = makeTgraph 
  [LD (1,2,3),RD (1,11,2),LD (1,4,5),RD (1,3,4),LD (1,10,11)
  ,RD (1,9,10),LK (9,1,7),RK (9,7,8),RK (5,7,1),LK (5,6,7)
  ]

To view the Tgraph we simply form a diagram (in this case 2 diagrams horizontally separated by 1 unit)

  hsep 1 [labelled drawj kingGraph, draw kingGraph]

and the result is shown in figure 2 with labels and dashed join edges (left) and without labels and join edges (right).

Figure 2: kingGraph with labels and dashed join edges (left) and without (right). — Figure 2: `kingGraph` with labels and dashed join edges (left) and without (right).

The boundary of the Tgraph consists of the edges of half-tiles which are not shared with another half-tile, so they go round untiled/external regions. The no crossing boundary constraint (equivalently, locally tile-connected) means that a boundary vertex has exactly two incident boundary edges and therefore has a single external angle in the tiling. This ensures we can always locally determine the relative angles of tiles at a vertex. We say a collection of half-tiles is a valid Tgraph if it constitutes a legal tiling but also satisfies the connectedness and no crossing boundaries constraints.

Our key operations on Tgraphs are $\small\texttt{decompose}$ , $\small\texttt{force}$ , and $\small\texttt{compose}$ which are illustrated in figure 3.

Figure 3 shows the kingGraph with its decomposition above it (left), the result of forcing the kingGraph (right) and the composition of the forced kingGraph (bottom right).

Decompose

An important property of Penrose dart and kite tilings is that it is possible to divide the half-tile faces of a tiling into smaller half-tile faces, to form a new (smaller scale) tiling.

Figure 4: Decomposition of (left) half-tiles

Figure 4 illustrates the decomposition of a left-dart (top row) and a left-kite (bottom row). With our Tgraph representation we simply introduce new vertices for dart and kite long edges and kite join edges and then form the new faces using these. This does not involve any geometry, because that is taken care of by drawing operations.

Force

Figure 5 illustrates the rules used by our $\small\texttt{force}$ operation (we omit a mirror-reflected version of each rule).

In each case the yellow half-tile is added in the presence of the other half-tiles shown. The yellow half-tile is forced because, by the legal tiling rules and the seven possible vertex types, there is no choice for adding a different half-tile on the edge where the yellow tile is added.

We call a Tgraph correct if it represents a tiling which can be continued infinitely to cover the whole plane without getting stuck, and incorrect otherwise. Forcing involves adding half-tiles by the illustrated rules round the boundary until either no more rules apply (in which case the result is a forced Tgraph) or a stuck tiling is encountered (in which case an incorrect Tgraph error is raised). Hence $\small\texttt{force}$ is a partial function but total on correct Tgraphs.

Compose: This is discussed in the next section.

2. Composition Problems and a Theorem

Compose Choices

For an infinite tiling, composition is a simple inverse to decomposition. However, for a finite tiling with boundary, composition is not so straight forward. Firstly, we may need to leave half-tiles out of a composition because the necessary parts of a composed half-tile are missing. For example, a half-dart with a boundary short edge or a whole kite with both short edges on the boundary must necessarily be excluded from a composition. Secondly, on the boundary, there can sometimes be a problem of choosing whether a half-dart should compose to become a half-dart or a half-kite. This choice in composing only arises when there is a half-dart with its wing on the boundary but insufficient local information to determine whether it should be part of a larger half-dart or a larger half-kite.

In the literature (see for example 1 and 2) there is an often repeated method for composing (also called inflating). This method always make the kite choice when there is a choice. Whilst this is a sound method for an unbounded tiling (where there will be no choice), we show that this is an unsound method for finite tilings as follows.

Clearly composing should preserve correctness. However, figure 6 (left) shows a correct Tgraph which is a forced queen, but the kite-favouring composition of the forced queen produces the incorrect Tgraph shown in figure 6 (centre). Applying our $\small\texttt{force}$ function to this reveals a stuck tiling and reports an incorrect Tgraph.

Figure 6: An erroneous and a safe composition

Our algorithm (discussed in Graphs, Kites and Darts) detects dart wings on the boundary where there is a choice and classifies them as unknowns. Our composition refrains from making a choice by not composing a half dart with an unknown wing vertex. The rightmost Tgraph in figure 6 shows the result of our composition of the forced queen with the half-tile faces left out of the composition (the remainder faces) shown in green. This avoidance of making a choice (when there is a choice) guarantees our composition preserves correctness.

Compose is a Partial Function

A different composition problem can arise when we consider Tgraphs that are not decompositions of Tgraphs. In general, $\small\texttt{compose}$ is a partial function on Tgraphs.

Figure 7: Composition may fail to produce a Tgraph

Figure 7 shows a Tgraph (left) with its sucessful composition (centre) and the half-tile faces that would result from a second composition (right) which do not form a valid Tgraph because of a crossing boundary (at vertex 6). Thus composition of a Tgraph may fail to produce a Tgraph when the resulting faces are disconnected or have a crossing boundary.

However, we claim that $\small\texttt{compose}$ is a total function on forced Tgraphs.

Compose Force Theorem

Theorem: Composition of a forced Tgraph produces a valid Tgraph.

We postpone the proof (outline) for this theorem to section 5. Meanwhile we use the result to establish relationships between $\small\texttt{compose}$ , $\small\texttt{force}$ , and $\small\texttt{decompose}$ in the next section.

3. Perfect Composition Theorem

In Graphs, Kites and Darts we produced a diagram showing relationships between multiple decompositions of a dart and the forced versions of these Tgraphs. We reproduce this here along with a similar diagram for multiple decompositions of a kite.

In figure 8 we show separate (apparently) commuting diagrams for the dart and for the kite. The bottom rows show the decompositions, the middle rows show the result of forcing the decompositions, and the top rows illustrate how the compositions of the forced Tgraphs work by showing both the composed faces (black edges) and the remainder faces (green edges) which are removed in the composition. The diagrams are examples of some commutativity relationships concerning $\small\texttt{force}$ , $\small\texttt{compose}$ and $\small\texttt{decompose}$ which we will prove.

It should be noted that these diagrams break down if we consider only half-tiles as the starting points (bottom right of each diagram). The decomposition of a half-tile does not recompose to its original, but produces an empty composition. So we do not even have $g = (\small\texttt{compose} \cdot \small\texttt{decompose}) \ g$ in these cases. Forcing the decomposition also results in an empty composition. Clearly there is something special about the depicted cases and it is not merely that they are wholetile complete because the decompositions are not wholetile complete. [Wholetile complete means there are no join edges on the boundary, so every half-tile has its other half.]

Below we have captured the properties that are sufficient for the diagrams to commute as in figure 8. In the proofs we use a partial ordering on Tgraphs (modulo vertex relabelling) which we define next.

Partial ordering of Tgraphs

If $g_0$ and $g_1$ are both valid Tgraphs and $g_0$ consists of a subset of the (half-tile) faces of $g_1$ we have

$\displaystyle g_0 \subseteq g_1$

which gives us a partial order on Tgraphs. Often, though, $g_0$ is only isomorphic to a subset of the faces of $g_1$ , requiring a vertex relabelling to become a subset. In that case we write

$\displaystyle g_0 \sqsubseteq g_1$

which is also a partial ordering and induces an equivalence of Tgraphs defined by

$\displaystyle g_0 \equiv g_1 \text{ if and only if } g_0 \sqsubseteq g_1 \text{ and } g_1 \sqsubseteq g_0$

in which case $g_0$ and $g_1$ are isomorphic as Tgraphs.

Both $\small\texttt{compose}$ and $\small\texttt{decompose}$ are monotonic with respect to $\sqsubseteq$ meaning:

$\displaystyle g_0 \sqsubseteq g_1 \text{ implies } \small\texttt{compose} \ g_0 \sqsubseteq \small\texttt{compose} \ g_1 \text{ and } \small\texttt{decompose} \ g_0 \sqsubseteq \small\texttt{decompose} \ g_1$

We also have $\small\texttt{force}$ is monotonic, but only when restricted to correct Tgraphs. Also, when restricted to correct Tgraphs, we have $\small\texttt{force}$ is non decreasing because it only adds faces:

$\displaystyle g \sqsubseteq \small\texttt{force} \ g$

and $\small\texttt{force}$ is idempotent (forcing a forced correct Tgraph leaves it the same):

$\displaystyle (\small\texttt{force} \cdot \small\texttt{force}) \ g \equiv \small\texttt{force} \ g$

Composing perfectly and perfect compositions

Definition: A Tgraph $g$ composes perfectly if all faces of $g$ are composable (i.e there are no remainder faces of $g$ when composing).

We note that the composed faces must be a valid Tgraph (connected with no crossing boundaries) if all faces are included in the composition because $g$ has those properties. Clearly, if $g$ composes perfectly then

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{compose}) \ g \equiv g$

In general, for arbitrary $g$ where the composition is defined, we only have

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{compose}) \ g \sqsubseteq g$

Definition: A Tgraph $g'$ is a perfect composition if $\small\texttt{decompose} \ g'$ composes perfectly.

Clearly if $g'$ is a perfect composition then

$\displaystyle (\small\texttt{compose} \cdot \small\texttt{decompose}) \ g' \equiv g'$

(We could use equality here because any new vertex labels introduced by $\small\texttt{decompose}$ will be removed by $\small\texttt{compose}$ ). In general, for arbitrary $g'$ ,

$\displaystyle (\small\texttt{compose} \cdot \small\texttt{decompose}) \ g' \sqsubseteq g'$

Lemma 1: $g'$ is a perfect composition if and only if $g'$ has the following 2 properties:

every half-kite with a boundary join has either a half-dart or a whole kite on the short edge, and
every half-dart with a boundary join has a half-kite on the short edge,

(Proof outline:) Firstly note that unknowns in $g$ (= $\small\texttt{decompose} \ g'$ ) can only come from boundary joins in $g'$ . The properties 1 and 2 guarantee that $g$ has no unknowns. Since every face of $g$ has come from a decomposed face in $g'$ , there can be no faces in $g$ that will not recompose, so $g$ will compose perfectly to $g'$ . Conversely, if $g'$ is a perfect composition, its decomposition $g$ can have no unknowns. This implies boundary joins in $g'$ must satisfy properties 1 and 2. $\square$

(Note: a perfect composition $g'$ may have unknowns even though its decomposition $g$ has none.)

It is easy to see two special cases:

If $g'$ is wholetile complete then $g'$ is a perfect composition.

Proof: Wholetile complete implies no boundary joins which implies properties 1 and 2 in lemma 1 which implies $g'$ is a perfect composition. $\square$
If $g'$ is a decomposition then $g'$ is a perfect composition.

Proof: If $g'$ is a decomposition, then every half-dart has a half-kite on the short edge which implies property 2 of lemma 1. Also, any half-kite with a boundary join in $g'$ must have come from a decomposed half-dart since a decomposed half-kite produces a whole kite with no boundary kite join. So the half-kite must have a half-dart on the short edge which implies property 1 of lemma 1. The two properties imply $g'$ is a perfect composition. $\square$

We note that these two special cases cover all the Tgraphs in the bottom rows of the diagrams in figure 8. So the Tgraphs in each bottom row are perfect compositions, and furthermore, they all compose perfectly except for the rightmost Tgraphs which have empty compositions.

In the following results we make the assumption that a Tgraph is correct, which guarantees that when $\small\texttt{force}$ is applied, it terminates with a correct Tgraph. We also note that $\small\texttt{decompose}$ preserves correctness as does $\small\texttt{compose}$ (provided the composition is defined).

Lemma 2: If $g_f$ is a forced, correct Tgraph then

$\displaystyle (\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose}) \ g_f \equiv g_f$

(Proof outline:) The proof uses a case analysis of boundary and internal vertices of $g_f$ . For internal vertices we just check there is no change at the vertex after $(\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose})$ using figure 12 (plus an extra case for the forced star). For boundary vertices we check the local context cases shown in figure 9.

Figure 9: Local contexts for boundary vertices of a forced Tgraph

This shows two cases for a kite origin, two cases for a kite opp, four cases for a kite wing, and four cases for a dart origin. The only case for a dart wing is one of the two kite opp cases and there are no dart opp cases as these cannot be on the boundary of a forced Tgraph. Actually figure 9 has a repeated case which is both a dart origin and a kite wing, but there are also 3 additional cases when we consider mirror images of those shown. Since there is no local change of the context in each case, and since this is true for all boundary vertices in any forced Tgraph, there can be no non-local change either. (We omit the full details). $\square$

Lemma 3: If $g'$ is a perfect composition and a correct Tgraph, then

$\displaystyle \small\texttt{force} \ g' \sqsubseteq (\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose}) \ g'$

(Proof outline:) The proof is by analysis of each possible force rule applicable on a boundary edge of $g'$ and checking local contexts to establish that (i) the result of applying $(\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose})$ to the local context must include the added half-tile, and (ii) if the added half tile has a new boundary join, then the result must include both halves of the new half-tile. The two properties of perfect compositions mentioned in lemma 1 are critical for the proof. However, since the result of adding a single half-tile may break the condition of the Tgraph being a pefect composition, we need to arrange that half-tiles are completed first then each subsequent half-tile addition is paired with its wholetile completion. This ensures the perfect composition condition holds at each step for a proof by induction. [A separate proof is needed to show that the ordering of applying force rules makes no difference to a final correct Tgraph (apart from vertex relabelling)]. $\square$

Lemma 4 If $g$ composes perfectly and is a correct Tgraph then

$\displaystyle \small\texttt{force} \ g \equiv (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose})\ g$

Proof: Assume $g$ composes perfectly and is a correct Tgraph. Since $\small\texttt{force}$ is non-decreasing (with respect to $\sqsubseteq$ on correct Tgraphs)

$\displaystyle \small\texttt{compose} \ g \sqsubseteq (\small\texttt{force} \cdot \small\texttt{compose}) \ g$

and since $\small\texttt{decompose}$ is monotonic

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{compose}) \ g \sqsubseteq (\small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose}) \ g$

Since $g$ composes perfectly, the left hand side is just $g$ , so

$\displaystyle g \sqsubseteq (\small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose}) \ g$

and since $\small\texttt{force}$ is monotonic (with respect to $\sqsubseteq$ on correct Tgraphs)

$\displaystyle (*) \ \ \ \ \ \small\texttt{force} \ g \sqsubseteq (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose}) \ g$

For the opposite direction, we substitute $\small\texttt{compose} \ g$ for $g'$ in lemma 3 to get

$\displaystyle (\small\texttt{force} \cdot \small\texttt{compose}) \ g \sqsubseteq (\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{compose}) \ g$

Then, since $(\small\texttt{decompose} \cdot \small\texttt{compose}) \ g \equiv g$ , we have

$\displaystyle (\small\texttt{force} \cdot \small\texttt{compose}) \ g \sqsubseteq (\small\texttt{compose} \cdot \small\texttt{force}) \ g$

Apply $\small\texttt{decompose}$ to both sides (using monotonicity)

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose}) \ g \sqsubseteq (\small\texttt{decompose} \cdot \small\texttt{compose} \cdot \small\texttt{force}) \ g$

For any $g''$ for which the composition is defined we have $(\small\texttt{decompose} \cdot \small\texttt{compose})\ g'' \sqsubseteq g''$ so we get

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose}) \ g \sqsubseteq \small\texttt{force} \ g$

Now apply $\small\texttt{force}$ to both sides and note $(\small\texttt{force} \cdot \small\texttt{force})\ g \equiv \small\texttt{force} \ g$ to get

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose}) \ g \sqsubseteq \small\texttt{force} \ g$

Combining this with (*) above proves the required equivalence. $\square$

Theorem (Perfect Composition): If $g$ composes perfectly and is a correct Tgraph then

$\displaystyle (\small\texttt{compose} \cdot \small\texttt{force}) \ g \equiv (\small\texttt{force} \cdot \small\texttt{compose}) \ g$

Proof: Assume $g$ composes perfectly and is a correct Tgraph. By lemma 4 we have

$\displaystyle \small\texttt{force} \ g \equiv (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose})\ g$

Applying $\small\texttt{compose}$ to both sides, gives

$\displaystyle (\small\texttt{compose} \cdot \small\texttt{force}) \ g \equiv (\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force} \cdot \small\texttt{compose})\ g$

Now by lemma 2, with $g_f = (\small\texttt{force} \cdot \small\texttt{compose}) \ g$ , the right hand side is equivalent to

$\displaystyle (\small\texttt{force} \cdot \small\texttt{compose}) \ g$

which establishes the result. $\square$

Corollaries (of the perfect composition theorem):

If $g'$ is a perfect composition and a correct Tgraph then

$\displaystyle \small\texttt{force} \ g' \equiv (\small\texttt{compose} \cdot \small\texttt{force} \cdot \small\texttt{decompose}) \ g'$

Proof: Let $g' = \small\texttt{compose} \ g$ (so $g \equiv \small\texttt{decompose} \ g'$ ) in the theorem. $\square$

[This result generalises lemma 2 because any correct forced Tgraph $g_f$ is necessarily wholetile complete and therefore a perfect composition, and $\small\texttt{force} \ g_f \equiv g_f$ .]
If $g'$ is a perfect composition and a correct Tgraph then

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{force}) \ g' \sqsubseteq (\small\texttt{force} \cdot \small\texttt{decompose}) \ g'$

Proof: Apply $\small\texttt{decompose}$ to both sides of the previous corollary and note that

$\displaystyle (\small\texttt{decompose} \cdot \small\texttt{compose}) \ g'' \sqsubseteq g'' \textit{ for any } g''$

provided the composition is defined, which it must be for a forced Tgraph by the Compose Force theorem. $\square$
If $g'$ is a perfect composition and a correct Tgraph then

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose}) \ g' \equiv (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force}) \ g'$

Proof: Apply $\small\texttt{force}$ to both sides of the previous corollary noting $\small\texttt{force}$ is monotonic and idempotent for correct Tgraphs

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force}) \ g' \sqsubseteq (\small\texttt{force} \cdot \small\texttt{decompose}) \ g'$

From the fact that $\small\texttt{force}$ is non decreasing and $\small\texttt{decompose}$ and $\small\texttt{force}$ are monotonic, we also have

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose}) \ g' \sqsubseteq (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force}) \ g'$

Hence combining these two sub-Tgraph results we have

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose}) \ g' \equiv (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{force}) \ g'$

$\square$

It is important to point out that if $g$ is a correct Tgraph and $\small\texttt{compose} \ g$ is a perfect composition then this is not the same as $g$ composes perfectly. It could be the case that $g$ has more faces than $(\small\texttt{decompose} \cdot \small\texttt{compose}) \ g$ and so $g$ could have unknowns. In this case we can only prove that

$\displaystyle (\small\texttt{force} \cdot \small\texttt{compose}) \ g \sqsubseteq (\small\texttt{compose} \cdot \small\texttt{force}) \ g$

As an example where this is not an equivalence, choose $g$ to be a star. Then its composition is the empty Tgraph (which is still a pefect composition) and so the left hand side is the empty Tgraph, but the right hand side is a sun.

Perfectly composing generators

The perfect composition theorem and lemmas and the three corollaries justify all the commuting implied by the diagrams in figure 8. However, one might ask more general questions like: Under what circumstances do we have (for a correct forced Tgraph $g_f$ )

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{compose}) \ g_f \equiv g_f$

Definition A generator of a correct forced Tgraph $g_f$ is any Tgraph $g$ such that $g \sqsubseteq g_f$ and $\small\texttt{force} \ g \equiv g_f$ .

We can now state that

Corollary If a correct forced Tgraph $g_f$ has a generator which composes perfectly, then

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{compose}) \ g_f \equiv g_f$

Proof: This follows directly from lemma 4 and the perfect composition theorem. $\square$

As an example where the required generator does not exist, consider the rightmost Tgraph of the middle row in figure 10. It is generated by the Tgraph directly below it, but it has no generator with a perfect composition. The Tgraph directly above it in the top row is the result of applying $(\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{compose})$ which has lost the leftmost dart of the Tgraph.

Figure 10: A Tgraph without a perfectly composing generator

We could summarise this section by saying that $\small\texttt{compose}$ can lose information which cannot be recovered by a subsequent $\small\texttt{force}$ and, similarly, $\small\texttt{decompose}$ can lose information which cannot be recovered by a subsequent $\small\texttt{force}$ . We have defined perfect compositions which are the Tgraphs that do not lose information when decomposed and Tgraphs which compose perfectly which are those that do not lose information when composed. Forcing does the same thing at each level of composition (that is it commutes with composition) provided information is not lost when composing.

4. Multiple Compositions

We know from the Compose Force theorem that the composition of a Tgraph that is forced is always a valid Tgraph. In this section we use this and the results from the last section to show that composing a forced, correct Tgraph produces a forced Tgraph.

First we note that:

Lemma 5: The composition of a forced, correct Tgraph is wholetile complete.

Proof: Let $g' = \small\texttt{compose} \ g_f$ where $g_f$ is a forced, correct Tgraph. A boundary join in $g'$ implies there must be a boundary dart wing of the composable faces of $g_f$ . (See for example figure 4 where this would be vertex 2 for the half dart case, and vertex 5 for the half-kite face). This dart wing cannot be an unknown as the half-dart is in the composable faces. However, a known dart wing must be either a large kite centre or a large dart base and therefore internal in the composable faces of $g_f$ (because of the force rules) and therefore not on the boundary in $g'$ . This is a contradiction showing that $g'$ can have no boundary joins and is therefore wholetile complete. $\square$

Theorem: The composition of a forced, correct Tgraph is a forced Tgraph.

Proof: Let $g' = \small\texttt{compose} \ g_f$ for some forced, correct Tgraph $g_f$ , then $g'$ is wholetile complete (by lemma 5) and therefore a perfect composition. Let $g = \small\texttt{decompose} \ g'$ , so $g$ composes perfectly ( $g' \equiv \small\texttt{compose} \ g$ ). By the perfect composition theorem we have

$\displaystyle (**) \ \ \ \ \ (\small\texttt{compose} \cdot \small\texttt{force}) \ g \equiv (\small\texttt{force} \cdot \small\texttt{compose}) \ g \equiv \small\texttt{force} \ g'$

We also have

$\displaystyle g = \small\texttt{decompose} \ g' = (\small\texttt{decompose} \cdot \small\texttt{compose}) \ g_f \sqsubseteq g_f$

Applying $\small\texttt{force}$ to both sides, noting that $\small\texttt{force}$ is monotonic and the identity on forced Tgraphs, we have

$\displaystyle \small\texttt{force} \ g \sqsubseteq \small\texttt{force} \ g_f \equiv g_f$

Applying $\small\texttt{compose}$ to both sides, noting that $\small\texttt{compose}$ is monotonic, we have

$\displaystyle (\small\texttt{compose} \cdot \small\texttt{force}) \ g \sqsubseteq \small\texttt{compose} \ g_f \equiv g'$

By (**) above, the left hand side is equivalent to $\small\texttt{force} \ g'$ so we have

$\displaystyle \small\texttt{force} \ g' \sqsubseteq g'$

but since we also have ( $\small\texttt{force}$ being non-decreasing)

$\displaystyle g' \sqsubseteq \small\texttt{force} \ g'$

we have established that

$\displaystyle g' \equiv \small\texttt{force} \ g'$

which means $g'$ is a forced Tgraph. $\square$

This result means that after forcing once we can repeatedly compose creating valid Tgraphs until we reach the empty Tgraph.

We can also use lemma 5 to establish the converse to a previous corollary:

Corollary If a correct forced Tgraph $g_f$ satisfies:

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{compose}) \ g_f \equiv g_f$

then $g_f$ has a generator which composes perfectly.

Proof: By lemma 5, $\small\texttt{compose} \ g_f$ is wholetile complete and hence a perfect composition. This means that $(\small\texttt{decompose} \cdot \small\texttt{compose}) \ g_f$ composes perfectly and it is also a generator for $g_f$ because

$\displaystyle (\small\texttt{force} \cdot \small\texttt{decompose} \cdot \small\texttt{compose}) \ g_f \equiv g_f$

$\square$

5. Proof of the Compose Force theorem

Theorem (Compose Force): Composition of a forced Tgraph produces a valid Tgraph.

Proof: For any forced Tgraph we can construct the composed faces. For the result to be a valid Tgraph we need to show no crossing boundaries and connectedness for the composed faces. These are proved separately by case analysis below.

Proof of no crossing boundaries

Assume $g_f$ is a forced Tgraph and that it has a non-empty set of composed faces (we can ignore cases where the composition is empty as the empty Tgraph is valid). Consider a vertex v in the composed faces of $g_f$ and first take the case that v is on the boundary of $g_f$ . We consider local contexts for a vertex v on a forced Tgraph boundary where the composition is non-empty as shown in figure 11.

Figure 11: Forced Boundary Vertex Compose Contexts

In each case v is shown as a red dot, and the composition is shown filled yellow. The cases for v are shown in rows: the first row is for dart origins, the second row is for kite origins, the third row is for kite wings, and the last rows is for kite opps. The dart wing cases are a subset of the kite opp cases, so not repeated, and dart opp vertices are excluded because they cannot be on the boundary of a forced Tgraph. We only show left-hand versions, so there is a mirror symmetric set for right-hand versions.

It is easy to see that there are no crossing boundaries of the composed faces at v in each case. Since any boundary vertex of any forced Tgraph (with a non-empty composition) must match one of these local context cases around the vertex, we can conclude that a boundary vertex of $g_f$ cannot become a crossing boundary in $compose \ g_f$ .

Next take the case where v is an internal vertex of $g_f$ .

Figure 12: Vertex types and their relationships

Figure 12 shows relationships between the forced Tgraphs of the 7 (internal) vertex types (plus a kite at the top right). The red faces are those around the vertex type and the black faces are those produced by forcing (if any). Each forced Tgraph has its composition directly above with empty compositions for the top row. We note that a (forced) star, jack, king, and queen vertex remains an internal vertex in the respective composition so cannot become a crossing boundary vertex. A deuce vertex becomes the centre of a larger kite and is no longer present in the composition (top right). That leaves cases for the sun vertex and ace vertex (=fool vertex). The sun Tgraph (sunGraph) and fool Tgraph (fool) consist of just the red faces at the respective vertex (shown top left and top centre). These both have empty compositions when there is no surrounding context. We thus need to check possible forced local contexts for sunGraph and fool.

The fool case is simple and similar to a duece vertex in that it is never part of a composition. [To see this consider inverting the decomposition arrows shown in figure 4. In both cases we see the half-dart opp vertex (labelled 4 in figure 4) is removed].

For the sunGraph there are only 7 local forced context cases to consider where the sun vertex is on the boundary of the composition.

Figure 13: Forced Contexts for a sun vertex v where v is on the composition boundary — Figure 13: Forced Contexts for a sun vertex `v` where `v` is on the composition boundary

Six of these are shown in figure 13 (the missing one is just a mirror reflection of the fourth case). Again, the relevant vertex v is shown as a red dot and the composed faces are shown filled yellow, so it is easy to check that there is no crossing boundary of the composed faces at v in each case. Every forced Tgraph containing an internal sun vertex where the vertex is on the boundary of the composition must match one of the 7 cases locally round the vertex.

Thus no vertex from $g_f$ can become a crossing boundary vertex in the composed faces and since the vertices of the composed faces are a subset of those of $g_f$ , we can have no crossing boundary vertex in the composed faces.

Proof of Connectedness

Assume $g_f$ is a forced Tgraph as before. We refer to the half-tile faces of $g_f$ that get included in the composed faces as the composable faces and the rest as the remainder faces. We want to prove that the composable faces are connected as this will imply the composed faces are connected.

As before we can ignore cases where the set of composable faces is empty, and assume this is not the case. We study the nature of the remainder faces of $g_f$ . Firstly, we note:

Lemma (remainder faces)

The remainder faces of $g_f$ are made up entirely of groups of half-tiles which are either:

Half-fools (= a half dart and both halves of the kite attached to its short edge) where the other half-fool is entirely composable faces, or
Both halves of a kite with both short edges on the ( $g_f$ ) boundary (so they are not part of a half-fool) where (at most) the origin is in common with composable faces, or
Whole fools where (at most) the shared kite origin in common with composable faces.

Figure 14: Remainder face groups (cases 1,2, and 3)

These 3 cases of remainder face groups are shown in figure 14. In each case the possible border in common with composable faces is shown yellow and the red edges are necessarily on the boundary of $g_f$ (the black boundary could be on the boundary of $g_f$ or shared with another reamainder face group). [A mirror symmetric version for the first group is not shown.] Examples can be seen in e.g. figure 13 where the first Tgraph has four examples of case 1, and two of case 2, the second has six examples of case 1 and two of case 2, and the fifth Tgraph has an example of case 3 as well as four of case 1. [We omit the detailed proof of this lemma which reasons about what gets excluded in a composition after forcing. However, all the local context cases are included in figure 15 (left-hand versions), where we only show those contexts where there is a non-empty composition.]

We note from the (remainder faces) lemma that the common boundary of the group of remainder faces with the composable faces (shown yellow in figure 14) is at most a single vertex in cases 2 and 3. In case 1, the common boundary is just a single edge of the composed faces which is made up of 2 adjacent edges of the composable faces that constitute the join of two half-fools.

This means each (remainder face) group shares boundary with exactly one connected component of the composable faces.

Next we establish that if two (remainder face) groups are connected they must share boundary with the same connected component of the composable faces. We need to consider how each (remainder face) group can be connected with a neighbouring such group. It is enough to consider forced contexts of boundary dart long edges (for cases 1 and 3) and boundary kite short edges (for case 2). The cases where the composition is non-empty all appear in figure 15 (left-hand versions) along with boundary kite long edges (middle two rows) which are not relevant for the proof.

Figure 15: Forced contexts for boundary edges

We note that, whenever one group of the remainder faces (half-fool, whole-kite, whole-fool) is connected to a neighbouring group of the remainder faces, any common boundary (shared edges and vertices) with the compososable faces is also connected. The combined common boundary forms either 2 adjacent composed face boundary edges (= 4 adjacent edges of the composable faces), or a composed face boundary edge and one of its end vertices, or a single composed face boundary vertex.

It follows that any connected collection of the remainder face groups shares boundary with a unique connected component of the composable faces. Since the collection of composable and remainder faces together is connected ( $g_f$ is connected) the removal of the remainder faces cannot disconnect the composable faces. For this to happen, at least one connected collection of remainder face groups would have to be connected to more than one connected component of composable faces.

This establishes connectedness of any composition of a forced Tgraph, and this completes the proof of the Compose Force theorem. $\square$

References

[2] Grünbaum B., Shephard G.C. (1987) Tilings and Patterns. W. H. Freeman and Company, New York. ISBN 0-7167-1193-1 (Hardback) (pages 540 to 542).

	PenroseKiteDart Anim… on Graphs, Kites and Darts
	PenroseKiteDart Anim… on Graphs, Kites and Darts…
	PenroseKiteDart Anim… on Graphs, Kites and Darts…
	PenroseKiteDart Anim… on PenroseKiteDart User Guide
	PenroseKiteDart User… on Graphs, Kites and Darts

readerunner

maths and computing experiments

Tag Archives: math

PenroseKiteDart Animations

About PenroseKiteDart

Decomposition Animations

A Composition Animation

Forcing Animations

Creating Animations

Crossfade tool

Force animation tool

Graphs, Kites and Darts – and Theorems

1. Quick Recap

2. Composition Problems and a Theorem

Compose Choices

Compose is a Partial Function

Compose Force Theorem

3. Perfect Composition Theorem

Partial ordering of Tgraphs

Composing perfectly and perfect compositions

Perfectly composing generators

4. Multiple Compositions

5. Proof of the Compose Force theorem

About PenroseKiteDart

Decomposition Animations

A Composition Animation

Forcing Animations

Creating Animations

Crossfade tool

Force animation tool

Previous related blogs

1. Quick Recap

2. Composition Problems and a Theorem

Compose Choices

Compose is a Partial Function

Compose Force Theorem

3. Perfect Composition Theorem

Partial ordering of Tgraphs

Composing perfectly and perfect compositions

Perfectly composing generators

4. Multiple Compositions

5. Proof of the Compose Force theorem