크기 타입

크기 타입 (Sized Types)

참고: 이것은 스텁(stub) 문서예요.

크기(size)는 정의 경계를 가로질러 데이터 구조의 깊이를 추적함으로써 종료 검사기를 돕는 역할을 해요.

크기용 내장 콤비네이터는 Sized types에서 설명돼요.

공유도를 위한 예제: 유한 언어 (Example for coinduction: finite languages)

Abel 2017과 Traytel 2017을 참고하세요.

결정 가능한(decidable) 언어는 무한 트리로 표현할 수 있어요. 각 노드는 알파벳 A의 문자 수만큼 자식을 가져요. 트리 루트에서 노드로의 각 경로는 언어에서 가능한 단어 하나를 결정해요. 각 노드는 불리언 레이블을 가지며, 그 레이블은 해당 노드에 대응하는 단어가 언어에 속할 때에만 true예요. 특히 트리의 루트 노드는 단어 ε가 언어에 속할 때에만 true로 레이블링돼요.

이 무한 트리는 다음과 같은 공유도 데이터 타입으로 표현할 수 있어요:

record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool
    δ : ∀{j : Size< i} → A → Lang j A

open Lang

앞서 말했듯 언어 a : Lang A가 주어지면, ν a ≡ true는 ε ∈ a일 때에만 성립해요. 반면 언어 δ a x : Lang A는 문자 x에 대한 a의 Brzozowski 도함수로, w ∈ δ a x는 xw ∈ a일 때에만 성립해요.

이 데이터 타입으로 몇 가지 정규 언어를 정의할 수 있어요. 첫 번째인 빈 언어는 단어를 전혀 포함하지 않아서 모든 노드가 false로 레이블링돼요:

∅ : ∀ {i A}  → Lang i A
ν ∅   = false
δ ∅ _ = ∅

두 번째는 단일 단어, 즉 빈 단어를 포함하는 언어예요. 루트 노드는 true로 레이블링되고 다른 모든 노드는 false로 레이블링돼요:

ε : ∀ {i A} → Lang i A
ν ε   = true
δ ε _ = ∅

두 언어의 합집합(또는 합)을 계산하려면 노드의 레이블에 대한 점별 or 연산을 해요:

_+_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (a + b)   = ν a   ∨ ν b
δ (a + b) x = δ a x + δ b x

infixl 10 _+_

이제 연결(concatenation)을 정의해 봐요.

기본 경우(ν)는 간단해요: ε ∈ a · b는 ε ∈ a이고 ε ∈ b일 때에만 성립해요.

도함수(δ)의 경우, 단어 w에 대해 w ∈ δ (a · b) x를 가정해 봐요. 이것은 xw = αβ를 의미하며, 여기서 α ∈ a이고 β ∈ b예요.

두 경우를 고려해야 해요:

• ε ∈ a. 그러면 다음 중 하나:
  • α = ε, 그리고 β = xw, 여기서 w ∈ δ b x.
  • α = xα', 여기서 α' ∈ δ a x, 그리고 w = α'β ∈ δ a x · b.
• ε ∉ a. 그러면 위의 두 번째 경우만 가능해요:
  • α = xα', 여기서 α' ∈ δ a x, 그리고 w = α'β ∈ δ a x · b.

_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (a · b)   = ν a ∧ ν b
δ (a · b) x = if ν a then δ a x · b + δ b x else δ a x · b

infixl 20 _·_

여기서 크기 타입이 정말 빛을 발해요. 크기 타입이 없으면 종료 검사기가 _+_나 if_then_else가 트리를 검사하지 않는다는 것을 인식하지 못해 정의가 비-생산적(non-productive)으로 렌더링될 수 있어요. 반대로 크기 타입이 있으면 a + b가 a와 b와 같은 깊이로 정의됨을 압니다.

비슷한 정신으로 Kleene 별을 정의할 수 있어요:

_* : ∀ {i A} → Lang i A → Lang i A
ν (a *)   = true
δ (a *) x = δ a x · a *

infixl 30 _*

다시, 타입이 _·_가 입력의 크기를 보존한다고 말해주므로 _·_에 대한 함수 호출 아래에서 a *에 대한 재귀 호출을 가질 수 있어요.

테스트 (Testing)

먼저 언어에서의 소속(membership)에 대한 정확한 개념을 주고 싶어요. 단어를 문자의 List로 간주해요.

_∈_ : ∀ {i} {A} → List i A → Lang i A → Bool
[]      ∈ a = ν a
(x ∷ w) ∈ a = w ∈ δ a x

소속을 테스트하는 단어의 크기는 언어 트리가 정의된 깊이보다 클 수 없다는 점에 주의하세요.

보통의, 비-크기 리스트를 사용하려면 언어의 크기가 ∞이기를 요청해야 해요.

_∈_ : ∀ {A} → List A → Lang ∞ A → Bool
[]      ∈ a = ν a
(x ∷ w) ∈ a = w ∈ δ a x

직관적으로 ∞는 Agda에서 정의할 수 있는 어떤 항의 크기보다도 큰 Size예요.

이제 이진 문자열을 단어로 생각해 봐요. 먼저 알파벳 A = Bool에 대해 길이 1의 단어 "x"를 포함하는 언어 ⟦ x ⟧를 정의해요:

⟦_⟧ : ∀ {i} → Bool → Lang i Bool
ν ⟦ _     ⟧       = false

δ ⟦ false ⟧ false = ε
δ ⟦ true  ⟧ true  = ε
δ ⟦ false ⟧ true  = ∅
δ ⟦ true  ⟧ false = ∅

이제 "true"와 "false" 문자가 교차하는 짝수 길이의 문자열로 구성된 bip-bop 언어를 정의할 수 있어요.

bip-bop = (⟦ true ⟧ · ⟦ false ⟧)*

bip-bop 언어에서 몇 개의 단어 소속을 테스트해 봐요!

test₁ : (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ []) ∈ bip-bop ≡ true
test₁ = refl

test₂ : (true ∷ false ∷ true ∷ false ∷ true ∷ []) ∈ bip-bop ≡ false
test₂ = refl

test₃ : (true ∷ true ∷ false ∷ []) ∈ bip-bop ≡ false
test₃ = refl

참고 문헌 (References)

• Equational Reasoning about Formal Languages in Coalgebraic Style, Andreas Abel.
• Formal Languages, Formally and Coinductively, Dmitriy Traytel, LMCS Vol. 13(3:28)2017, pp. 1–22 (2017).

더 알아보기 (Learn more)

• Agda 문서: 크기 타입 원문