공유도(coinduction)

공유도(coinduction) (Coinduction)

아래의 공재귀(corecursive) 정의는 --guardedness 옵션이 활성화되어 있을 때 받아들여져요:

{-# OPTIONS --guardedness #-}

(다른 접근 방식으로는 Sized Type을 사용하는 방법이 있어요.)

공유도 레코드 (Coinductive Records)

어떤 타입 A의 원소들로 이루어진 무한 리스트(또는 스트림) 타입을 다음과 같이 정의할 수 있어요:

record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A

귀납 레코드 타입과 달리, 레코드를 구성하는 필드를 정의하기 전에 키워드 coinductive를 도입해야 해요.

레코드 타입 Stream에 명시적 생성자를 줄 필요가 없다는 점이 흥미로워요.

이제 코패턴(copatterns)을 사용해 주어진 원소 a를 무한히 반복하는 스트림 같은 것을 만들 수 있어요:

repeat : {A : Set} (a : A) -> Stream A
hd (repeat a) = a
tl (repeat a) = repeat a

또한 한 쌍의 스트림에 대한 점별 동일성(이중시뮬레이션 bisimulation이자 동치 관계 equivalence)을 공유도 레코드로 정의할 수 있어요:

record _≈_ {A} (xs : Stream A) (ys : Stream A) : Set where
  coinductive
  field
    hd-≡ : hd xs ≡ hd ys
    tl-≈ : tl xs ≈ tl ys

코패턴을 사용하면 한쪽은 짝수 위치의 원소를 반환하고 다른 한쪽은 홀수 위치의 원소를 반환하는 스트림 함수 한 쌍을 정의할 수 있어요:

even : ∀ {A} → Stream A → Stream A
hd (even xs) = hd xs
tl (even xs) = even (tl (tl xs))

odd : ∀ {A} → Stream A → Stream A
odd xs = even (tl xs)

split : ∀ {A} → Stream A → Stream A × Stream A
split xs = even xs , odd xs

또한 한 쌍의 스트림의 원소를 교차시켜 병합하는 함수도 있어요:

merge : ∀ {A} → Stream A × Stream A → Stream A
hd (merge (xs , ys)) = hd xs
tl (merge (xs , ys)) = merge (ys , tl xs)

마지막으로, merge가 split의 왼쪽 역원임을 증명할 수 있어요:

merge-split-id : ∀ {A} (xs : Stream A) → merge (split xs) ≈ xs
hd-≡ (merge-split-id _)  = refl
tl-≈ (merge-split-id xs) = merge-split-id (tl xs)

공유도 레코드 생성자 (Coinductive Record Constructors)

Stream 같은 공유도 레코드 타입에 명시적 생성자를 줄 수 있어요:

record Stream' (A : Set) : Set where
  coinductive
  constructor cons
  field
    hd : A
    tl : Stream' A

하지만 이 생성자는 패턴 매칭할 수 없어요:

-- 스트림의 세 번째 원소 구하기
third : ∀{A} → Stream' A → A

-- 허용되지 않음:
-- third (cons _ (cons _ (cons x _))) = x

대신 레코드 필드를 projection으로 사용할 수 있어요:

third str = str .tl .tl .hd

생성자는 정의의 오른쪽 변에서 평소처럼 사용할 수 있어요:

-- 스트림 앞에 리스트를 붙이기
prepend : ∀{A} → List A → Stream' A → Stream' A
prepend [] str = str
prepend (a ∷ as) str = cons a (prepend as str)

하지만 이 생성자는 생산성(productivity) 검사기의 '가드(guarding)'로 간주되지 않아요:

-- 하나의 원소를 영원히 반복하는 스트림 만들기
cycle : ∀{A} → A → Stream' A

-- 종료 검사를 통과하지 못함:
-- cycle a = cons a (cycle a)

대신 코패턴 매칭을 사용할 수 있어요:

cycle a .hd = a
cycle a .tl = cycle a

패턴 람다에서 코패턴을 사용하는 것도 가능해요:

cycle' : ∀{A} → A → Stream' A
cycle' a = λ where
  .hd → a
  .tl → cycle' a

이 제한 사항에 대한 자세한 내용은 이 풀 리퀘스트와 이 커밋을 참고하세요.

ETA_EQUALITY 프래그마

Agda는 공유도 레코드 선언에서 eta-equality 지시를 허용하지 않아요. 그 이유는 공유도 타입에 대한 η는 일반적으로 불안전하고 타입 체커가 무한 루프에 빠질 수 있기 때문이에요.

예를 들어 다음 코드는 test를 검사할 때 무한 η 확장으로 이어질 것이에요:

record R : Set where
 coinductive; eta-equality
 field force : R
open R

foo : R
foo .force .force = foo

test : foo .force ≡ foo
test = refl

무엇을 하고 있는지 안다면, ETA_EQUALITY 프래그마를 사용해 Agda를 오버라이드하고 공유도 레코드가 η를 지원하도록 강제할 수 있어요.

{-# ETA_EQUALITY #-}
record R : Set where
  ...

옛 공유도 (Old Coinduction)

참고: 이것은 Agda에서 공유도를 지원하는 옛 방식이에요. 공유도 레코드(Coinductive Records)를 사용하는 것이 권장돼요.

공유도를 사용하려면 표준 라이브러리에서 Coinduction 모듈을 임포트하는 것이 좋아요. 그러면 지연 연산자 ∞로 공유도 발생을 표시해 공유도 타입을 정의할 수 있어요:

data Coℕ : Set where
   zero : Coℕ
   suc  : ∞ Coℕ → Coℕ

타입 ∞ A는 타입 A의 일시 중단된 계산으로 볼 수 있어요. 여기에는 delay와 force 함수가 함께 제공돼요:

♯_ : ∀ {a} {A : Set a} → A → ∞ A
♭  : ∀ {a} {A : Set a} → ∞ A → A

공유도 타입의 값은 종료할 필요는 없지만 생산적이어야 하는 공재귀(corecursion)로 구성할 수 있어요. 생산성의 근사치로서 종료 검사기는 공재귀 정의가 공유도 생성자로 가드되어야 한다고 요구해요. 예를 들어 무한 "자연수"는 다음과 같이 정의할 수 있어요:

inf : Coℕ
inf = suc (♯ inf)

가드된 공재귀 검사는 크기-변화 종료(size-change termination) 검사와 통합되어 있어, 귀납 타입과 공유도 타입의 흥미로운 조합을 허용해요. 예를 들어 스트림 프로세서 타입과 몇몇 함수를 정의할 수 있어요:

-- 무한 스트림.

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

-- 스트림 프로세서 SP A B는 A의 원소를 소비하고 B의
-- 원소를 생산합니다. B를 생산하기 전에 유한한 개수의 A만 소비할 수 있습니다.

data SP (A B : Set) : Set where
  get : (f : A → SP A B) → SP A B
  put : (b : B) (sp : ∞ (SP A B)) → SP A B

-- 함수 eat는 Stream B로의 외부 공재귀와 SP A B에 대한
-- 내부 재귀로 정의됩니다.

eat : ∀ {A B} → SP A B → Stream A → Stream B
eat (get f)    (a ∷ as) = eat (f a) (♭ as)
eat (put b sp) as       = b ∷ ♯ eat (♭ sp) as

-- 스트림 프로세서의 합성.

_∘_ : ∀ {A B C} → SP B C → SP A B → SP A C
get f₁    ∘ put x sp₂ = f₁ x ∘ ♭ sp₂
put x sp₁ ∘ sp₂       = put x (♯ (♭ sp₁ ∘ sp₂))
sp₁       ∘ get f₂    = get (λ x → sp₁ ∘ f₂ x)

"공유도 패밀리(coinductive families)"를 정의하는 것도 가능해요. 생성자의 인덱스 표현식에서 delay 생성자(♯_)를 사용하지 않는 것이 권장돼요. 공유도 "자연수" 사이의 동일성에 대한 다음 정의는 권장되지 않아요:

data _≈’_ : Coℕ → Coℕ → Set where
  zero : zero ≈’ zero
  suc  : ∀ {m n} → ∞ (m ≈’ n) → suc (♯ m) ≈’ suc (♯ n)

권장되는 정의는 다음과 같아요:

data _≈_ : Coℕ → Coℕ → Set where
  zero : zero ≈ zero
  suc  : ∀ {m n} → ∞ (♭ m ≈ ♭ n) → suc m ≈ suc n

더 알아보기 (Learn more)

• Agda 문서: 공유도 원문