[Agda] Some observations about μν

[Nils Anders Danielsson]

Hi,

I recently realised that nested fixpoints of the form μX.νY.… cannot be
encoded directly in Agda. Consider the following example (due to
Christophe Raffalli):

  μO.νZ.Z + O

This essentially encodes bit streams (read Z as zero and O as one) with
an infinite number of zeros but only a finite number of ones:
(0^⋆1)^⋆0^ω. You might believe that this type can be encoded in two
steps in Agda. First the inner fixpoint:

  data Z (O : Set) : Set where
    [0] : ∞ (Z O) → Z O
    [1] :    O    → Z O

Then the outer fixpoint:

  data O : Set where
    ↓ : Z O → O

However, it is still possible to define values of the form (01)^ω:

  01^ω : O
  01^ω = ↓ ([0] (♯ [1] 01^ω))

The reason is the way the termination/productivity checker works: it
accepts definitions by guarded corecursion as long as the guard contains
at least one occurrence of ♯_, no matter how the types involved are
defined. In effect ∞ has global reach, and all mixed fixpoints should be
read as νX.μY.….

Thorsten Altenkirch and I have discussed this problem, and we have not
yet decided whether the observation above points to a problem or not. If
one takes the view that the ideal semantics of Agda is the one where ∞
is read as domain-theoretic lifting, and the elements of a type are the
/total/ elements of the solution to the relevant domain-theoretic
equation, then there is no problem. Consider the types μO.νZ.Z + O and
νZ.μO.Z + O. The corresponding domain-theoretic expressions are

  μO. μZ. Z_⊥ + O

and

  μZ. μO. Z_⊥ + O,

and these are equivalent.

Some open questions:

* Are there any good applications of μX.νY.…? Note that the proof
  principles you get from such types are rather weak. For instance, for
  μO.νZ.Z + O you cannot prove that there has to be a suffix consisting
  only of zeros. You can prove negative statements like "(01)^ω is not a
  member of this type", though.

* Can μX.νY.… be encoded in Agda? In the example above, note that

    List Bit × Stream Unit

  is not isomorphic to μO.νZ.Z + O, because for elements of the former
  type you can decide when you have seen the last occurrence of the
  digit one.

* Is Agda consistent? It would be unfortunate if we could find a
  property which is true for the encoding of μO.νZ.Z + O given above,
  but not true for the obvious encoding of νZ.μO.Z + O.

One way out of this situation, suggested by Thorsten, is to disallow
types which are seemingly defined as μX.F where F mentions X under ∞
(like O above).

Further details can be found in
http://www.cs.nott.ac.uk/~nad/listings/codata/MuNu.html.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.