Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 2

Swap the components of every ordered pair using a list comprehension:

invert :: [(a, a)] -> [(a, a)]
invert r = [(y, x) | (x, y) <- r]

Thus

invert (R) = R^{- 1}

, the converse relation. Swapping is a bijection, since doing it twice restores the original pair. Therefore distinct input pairs remain distinct; no equality constraint or duplicate removal is necessary.

b

 0  0

Solution

 0  0

Retain the first element, filter all its further occurrences out of the tail, and recurse:

removedup :: Eq a => [a] -> [a]
removedup []     = []
removedup (x:xs) = x : removedup (filter (/= x) xs)

The boxed specification is

each distinct input value occurs once, in first-occurrence order

. The Haskell type class Eq is needed for comparing values. Structural induction on a finite list proves duplicate removal: filtering removes every further x, and the recursive result contains each remaining distinct value exactly once. In the worst case of all distinct values, successive filters give quadratic time complexity.

c

 0  0

Solution

 0  0

Use the first binary relation for the outer generator, the second for the inner generator, and match their middle values. Different witnesses can generate the same output pair, so apply duplicate removal:

relcomp :: Eq a => [(a, a)] -> [(a, a)] -> [(a, a)]
relcomp r s = removedup [(a, b) | (a, c) <- r,
                                (d, b) <- s, c == d]

The guards give precisely the existential witness required for composition of relations:

(a, b) \in relcomp (R, S) ⟺ \exists c : (a, c) \in R \land (c, b) \in S .

(1)

Every output is sound by its generating witness, and every witness is visited for finite inputs. Duplicate removal converts the resulting enumeration back to the required representation by distinct pairs.

d

 0  0

Solution

 0  0

Maintain all pairs discovered so far. Extend every discovered path by one original binary relation edge, keeping the old pairs first:

transclose :: Eq a => [(a, a)] -> [(a, a)]
transclose r = grow (removedup r)
  where
    grow s =
      let t = removedup (s ++ relcomp r s)
      in if length t == length s then s else grow t

After

j

extensions, the represented binary relation is

R \cup R^{2} \cup \dots \cup R^{j + 1}

. This loop invariant follows by distributivity of composition of relations over a union. The old list s is a duplicate-free prefix of t; therefore equality of lengths is equivalent to equality of the represented sets and signals a fixed point.

Let

V

be the finite set of endpoints appearing in the input. No extension introduces a new endpoint, so there are at most

∣ V ∣^{2}

distinct pairs. Every nonfinal iteration adds at least one pair, proving algorithm termination. At the fixed point

S

, we have

R \subseteq S

and

R; S \subseteq S

. Mathematical induction gives

R^{i} \subseteq S

for every positive

i

, while the loop invariant says that each discovered pair belongs to some

R^{i}

. Hence

transclose (R) = R^{+} = i \geq 1 ⋃ R^{i} .

(1)

This is the transitive closure of a relation, rather than a reflexive closure: diagonal pairs appear only when supported by nonempty cycles. The empty input is handled immediately.

e

 0  0

Solution

 0  0

The answer depends on the actual definitions above, especially the direction used for duplicate removal.

invert works for an infinite binary relation enumerated by a lazy list: each output needs only one input pair, and swapping preserves distinctness.
removedup is productive whenever the input has infinitely many distinct values and equality tests terminate. Each next new value occurs at a finite input position and passes finitely many earlier filters. In particular, it works on the stipulated distinct-element representation of an infinite binary relation. On an infinite list with only finitely many distinct values it emits those values but cannot certify that there is no next new value; for example, demanding the tail after the first result of removedup (repeat 1) diverges.
relcomp does not work for arbitrary infinite inputs. Its nested list comprehension can remain forever in the inner generator. With r = [(i,0) | i <- [0..]] and s = [(0,j) | j <- [0..]], it emits only pairs whose first component is zero, starving every later outer value. Duplicate removal cannot repair this lack of fair enumeration.
transclose does not work for a general infinite input: even its first length s cannot finish. It waits for finite saturation before returning any result.

Thus

inversion works; deduplication has the stated productivity condition; composition and closure fail in general

. A fairer enumeration may improve the latter constructions, but would be a different algorithm; ordinary depth-first enumeration does not become fair through lazy evaluation alone.

 Ancestors (10)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 2

 Discussion (0)  Subscribe (1) New discussion

 Discussion (0) New discussion