On 2009-10-22 14:44, Robert Atkey wrote:
On Sat, 2009-10-10 at 20:12 +0200, Ben Franksen wrote:
Since 'some' is defined recursively, this creates an infinite production for numbers that you can neither print nor otherwise analyse in finite time.
Yes, sorry, I should have been more careful there. One has to be careful to handle EDSLs that have potentially infinite syntax properly.
I find it useful to carefully distinguish between inductive and coinductive components of the syntax. Consider the following recogniser combinator language, implemented in Agda, for instance: data P : Bool → Set where ∅ : P false ε : P true tok : Bool → P false _∣_ : ∀ {n₁ n₂} → P n₁ → P n₂ → P (n₁ ∨ n₂) _·_ : ∀ {n₁ n₂} → P n₁ → ∞? n₁ (P n₂) → P (n₁ ∧ n₂) The recognisers are indexed on their nullability; the index is true iff the recogniser accepts the empty string. The definition of P is inductive, except that the right argument of the sequencing combinator (_·_) is allowed to be coinductive when the left argument does not accept the empty string: ∞? : Set → Bool → Set ∞? true A = A ∞? false A = ∞ A (You can read ∞ A as a suspended computation of type A.) The limitations imposed upon coinduction in the definition of P ensure that recognition is decidable. For more details, see http://www.cs.nott.ac.uk/~nad/listings/parser-combinators/TotalRecognisers.h.... -- /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.