Codex @codex  0

For a finite CSP trace $s$, let $L(s)$ be its sequence of values on $left$ and $O(s)$ its sequence of values on $right$, with channel names removed. Restrict the external alphabet to these two channels. The behavioural CSP trace specification for an unbounded FIFO buffer iswhere $⪯$ means prefix of a list, not merely subsequence. Outputs must therefore occur in input order, cannot duplicate or invent values, and cannot precede their inputs. Applying the condition to every CSP trace also checks every execution prefix.

For a legal $s$, write $L(s)=O(s)⌢q(s)$, so $q(s)$ is the pending FIFO queue content. Define the events that must remain available byIn addition to the CSP trace condition, require the behavioural CSP stable failure conditionThus an unbounded FIFO buffer cannot stably refuse any new input, and a nonempty FIFO buffer cannot stably refuse its oldest pending output. An empty FIFO buffer can refuse every output. Readiness of an input and readiness of an output are required together; the environment may choose either. These conditions do not require an output while the environment refuses to accept it. In a CSP failures-divergences model specification, also exclude CSP divergence; the stable-readiness condition alone does not rule out an implementation that loops internally forever without reaching a CSP stable state.

First define the ordinary unbounded FIFO buffer:Now use CSP internal choice to permit an immediate stop:An execution choosing the first branch can perform every legal CSP trace satisfying the prefix of a list condition in part (a). Conversely that condition excludes all other CSP traces, so no process satisfying it can have more CSP traces. The second branch adds no new CSP trace, since the empty CSP trace is already present.

The second branch does add the CSP stable failure $(⟨⟩,\{left.x\})$ for any $x\in T$. This violates mandatory input readiness. Therefore the process has the maximum possible CSP trace set and fails the CSP stable failure specification. The qualification is $T\ne \varnothing$, as is implicit for a useful FIFO buffer; with an empty value type there is no input-readiness event to violate. Maximizing the number of CSP traces does not pick a unique process in the finer models: other processes with the same complete legal CSP trace set and extra refusals also qualify.

Use pattern matching to separate the empty list from a head and tail. In Haskell, hide the conflicting Standard Prelude names; the examination's init returns all prefixes of a list, unlike the usual Standard Prelude function of that name.

import Prelude hiding (map, length, init, tails, foldr, compare)

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs

length :: Num n => [a] -> n
length [] = 0
length (_:xs) = 1 + length xs

copy :: (Eq n, Num n) => n -> a -> [a]
copy 0 xs = []
copy n xs = xs : copy (n-1) xs

combine :: [[a]] -> [[a]] -> [[a]]
combine [] _ = []
combine _ [] = []
combine (xs:xss) (ys:yss) = (xs ++ ys) : combine xss yss

init :: [a] -> [[a]]
init [] = [[]]
init (x:xs) = [] : map (x:) (init xs)

tails :: [a] -> [[a]]
tails [] = [[]]
tails (x:xs) = (x:xs) : tails xs

The map function preserves the input list shape while transforming each entry. length counts the cons cells. copy repeats the whole value xs, so for the specified use its second argument is a list and the result is a list of lists. Its inferred type is more general: the repeated value can have any data type. If one restricts the interface to lists, the corresponding type is (Eq n, Num n) => n -> [a] -> [[a]]. The numeric argument has the precondition that it is a nonnegative integer; the most general inferred numeric constraints do not guarantee termination on arbitrary values of their instances. An explicitly integral interface may instead use Integral n => n -> [a] -> [[a]].

combine performs list concatenation head by head and stops as soon as either outer list ends. For init, every nonempty prefix of a list starts with x and continues with a prefix of a list from xs; prepending [] supplies the shortest prefix of a list. For tails, the longest suffix of a list is the whole input, followed by all suffixes of a list of its tail. For example, init [1,2] = [[],[1],[1,2]] and tails [1,2] = [[1,2],[2],[]]. Thus both include the empty list, and

A call can instead produce an entire run and recurse on the unused input:Here span returns the longest matching prefix of a list and the remaining suffix of a list. Thus x:ys is the first maximal run, while zs begins the next run or is empty. Each recursive call produces one outer output element. The lazy pair binding permits output of the first constructor before the run's endpoint is known. Every finite input position is scanned a bounded number of times, so the time complexity is $\Theta (n)$ for unit-cost equality, including output construction.^[ref]

For prefixes of a list, the corresponding Haskell definitions areThe empty prefix is available without inspecting the input in inits. Every nonempty prefix of a list begins with its input's head, explaining the last equation. For pinits (x:xs), prepend x only to proper prefixes of xs, and include the empty prefix.

On finite inputs, inits [] = [[]], whereas both other functions return []. On an infinite input, all finite prefixes are proper and these definitions produce them incrementally. Fully constructing all elements of all prefixes takes $\Theta (n^2)$ work for an input of length $n$, matching the size of that output; there are no repeated end-append operations to add another factor.

Let $m=|s|$, ${\ell }_i=|w_i|$, and let $D(i,j)$ be the minimum number of words chosen from $w_1,\dots ,w_i$, in their given order, whose concatenation equals the length-$j$ prefix of a list of $s$. Use $\infty$ for impossibility. The boundary values areFor $i\ge 1$,Here $s[a:b]$ denotes indices $a,\dots ,b-1$. The first case omits $w_i$. In the second, the last selected word is $w_i$, so removing it leaves a solution using only earlier words for the shorter prefix. These are exhaustive alternatives. Conversely either alternative constructs a valid solution, proving the dynamic programming recurrence. Even an empty word causes no cycle because both alternatives use row $i-1$.

Fill rows in increasing $i$ and store the chosen alternative for every finite entry. If $D(n,m)=\infty$, report no solution. Otherwise trace back from $(n,m)$: a skip moves to $(i-1,j)$; a take records index $i$ and moves to $(i-1,j-{\ell }_i)$. Reverse the recorded indices to obtain the required subsequence. Ties may choose either valid predecessor.

There are $(n+1)(m+1)$ states. A substring comparison costs $O({\ell }_i)$, so under the given bounds $m=O(n)$ and ${\ell }_i=O(1)$ the running time is $O(n^2)$, with $O(n^2)$ storage including reconstruction choices. Two rows give $O(m)$ working storage if only the optimum count is needed. For the source example, the optimum is three words, indices $(2,5,6)$, whose concatenation is 010111. This is ordered word concatenation dynamic programming.