-- Autumn school "Proof and Computation" -- 3-8 October 2016 -- Fischbachau, Bayern, DE -- -- Andreas Abel, Agda Tutorial -- -- Part 2: Formal languages, coinductively treated via copatterns module CopatternsSolution where open import Data.Nat.Base open import Data.Bool.Base open import Relation.Binary.PropositionalEquality open import Size module Streams where -- Streams record Stream (A : Set) : Set where coinductive field head : A tail : Stream A open Stream -- Constructor cons : {A : Set} (a : A) (as : Stream A) → Stream A head (cons a as) = a tail (cons a as) = as -- Repetition repeat : {A : Set} (a : A) → Stream A -- repeat a = cons a (repeat a) head (repeat a) = a tail (repeat a) = repeat a -- C-c C-c split on result -- Stream zipping zipWith : {A B C : Set} (f : A → B → C) (s : Stream A) (t : Stream B) → Stream C head (zipWith f s t) = f (head s) (head t) tail (zipWith f s t) = zipWith f (tail s) (tail t) evil : Stream ℕ → Stream ℕ → Stream ℕ evil s t = tail t -- Fibonacci {-# TERMINATING #-} fib : Stream ℕ head fib = 0 head (tail fib) = 1 tail (tail fib) = zipWith (_+_) fib (tail fib) -- Termination hinges on the continuity of zipWith. -- Compare with the similarly structured rhs -- tail (tail fib) = evil fib (tail fib) -- to understand why Agda refuses to certify termination -- in the untyped termination checker. module SizedStreams where -- Streams record Stream (i : Size) (A : Set) : Set where coinductive field head : A tail : ∀{j : Size< i} → Stream j A open Stream -- Constructor cons : {i : Size} {A : Set} (a : A) (as : Stream i A) → Stream (↑ i) A head (cons a as) = a tail (cons a as) = as -- Repetition repeat : {i : Size} {A : Set} (a : A) → Stream i A -- repeat {i} a = cons {i} a (repeat {i} a) head (repeat a) = a tail (repeat {i} a) {j} = repeat {j} a -- C-c C-c split on result -- Stream zipping zipWith : ∀ {i A B C} (f : A → B → C) (s : Stream i A) (t : Stream i B) → Stream i C head (zipWith f s t) = f (head s) (head t) tail (zipWith {i} f s t) {j} = zipWith f (tail s {j}) (tail t {j}) -- evil : ∀{i} → Stream i ℕ → Stream i ℕ → Stream i ℕ -- evil s t = tail t -- Fibonacci fib : ∀{i} → Stream i ℕ head fib = 0 head (tail fib) = 1 -- tail (tail fib) = evil fib (tail fib) tail (tail (fib {i}) {j}) {k} = zipWith (_+_) (fib {k}) (tail (fib {j})) module Languages where -- Decidable language record Lang (A : Set) : Set where coinductive field ν : Bool δ : A → Lang A open Lang -- empty language ∅ : ∀{A} → Lang A ν ∅ = false δ ∅ a = ∅ -- empty word ε : ∀{A} → Lang A ν ε = true δ ε x = ∅ -- union infixl 4 _∪_ _∪_ : ∀{A} (l k : Lang A) → Lang A ν (l ∪ k) = ν l ∨ ν k δ (l ∪ k) x = δ l x ∪ δ k x -- concatenation -- infixl 6 _∙_ -- _∙_ : ∀{A} (l k : Lang A) → Lang A -- ν (l ∙ k) = ν l ∧ ν k -- δ (l ∙ k) x = if ν l then δ l x ∙ k ∪ δ k x else δ l x ∙ k -- star -- infixr 15 _* -- _* : ∀{A} (l : Lang A) → Lang A -- l * = {!!} module SizedLanguages where -- Decidable language record Lang (i : Size) (A : Set) : Set where coinductive field ν : Bool δ : ∀{j : Size< i} → A → Lang j A open Lang -- empty language ∅ : ∀{i A} → Lang i A ν ∅ = false δ ∅ a = ∅ -- empty word ε : ∀{i A} → Lang i A ν ε = true δ ε x = ∅ -- union infixl 4 _∪_ _∪_ : ∀{i A} (l k : Lang i A) → Lang i A ν (l ∪ k) = ν l ∨ ν k δ (l ∪ k) x = δ l x ∪ δ k x -- concatenation infixl 6 _∙_ _∙_ : ∀{i A} (l k : Lang i A) → Lang i A ν (l ∙ k) = ν l ∧ ν k δ (l ∙ k) x = if ν l then δ l x ∙ k ∪ δ k x else δ l x ∙ k -- star infixr 15 _* _* : ∀{i A} (l : Lang i A) → Lang i A ν (l *) = true δ (l *) x = δ l x ∙ l * -- δ (l *) x = δ (ε ∪ l ∙ l *) x -- = δ ε x ∪ δ (l ∙ l *) x -- = ∅ ∪ δ l x ∙ l * ∪ (if ν l then δ (l *) x else ∅) -- = δ l x ∙ l * ∪ (if ν l then δ (l *) x else ∅)