잠정 정의

잠정 정의 (Provisional Definitions)

때로는 의존 타입으로 프로그래밍할 때, 타입 검사기가 요구하는 타입과 우리가 작성한 프로그램의 타입이 다를 수 있어요 (정규 형식이 같지 않다는 점에서), 하지만 그럼에도 증명 가능하게 같을 수 있어요. 예를 들어 parity 함수를 떠올려보세요:

data Parity : Nat -> Type where
   Even : Parity (n + n)
   Odd  : Parity (S (n + n))

이것을 다음과 같이 구현하고 싶어요:

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = Even {n=S j}
  parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}

이것은 단순히 0은 짝수, 1은 홀수, 그리고 재귀적으로 k+2의 parity는 k의 parity와 같다고 진술해요. n의 값을 even과 odd로 명시적으로 표시하는 것은 타입 추론을 돕는 데 필요해요.

안타깝게도 타입 검사기는 이것을 거부해요:

viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:
Type mismatch between
    Parity (plus (S j) (S j))
and
    Parity (S (S (plus j j)))

Specifically:
    Type mismatch between
        plus (S j) (S j)
    and
        S (S (plus j j))

타입 검사기는 (j+1)+(j+1)과 2+j+j가 같은 값으로 정규화되지 않는다고 알려줘요. 이것은 plus가 첫 번째 인자에 대해 재귀적으로 정의되고, 두 번째 값에서는 두 번째 인자에 후임자 기호가 있기 때문에 축소에 도움이 되지 않기 때문이에요. 이 값들은 분명히 같아요 — 이 문제를 고치도록 프로그램을 어떻게 다시 쓸까요?

잠정 정의 (Provisional definitions)

잠정 정의는 증명 세부 사항을 더 나중 시점까지 미룰 수 있게 해서 이 문제를 도와줘요. 유용한 주된 두 가지 이유가 있어요.

프로토타이핑할 때, 증명의 모든 세부 사항을 끝내기 전에 프로그램을 테스트할 수 있는 것이 유용함.
프로그램을 읽을 때, 독자가 밑바탕의 알고리즘에서 주의를 분산시키지 않도록 증명 세부 사항을 미루는 것이 훨씬 명확한 경우가 많음.

잠정 정의는 오른쪽을 = 대신 ?=로 도입한다는 점을 제외하면 일반 정의와 같은 방식으로 작성돼요. 우리는 parity를 다음과 같이 정의해요:

parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j))) | Even ?= Even {n=S j}
  parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

이 형태로 작성하면, 타입 오류를 보고하는 대신 Idris는 타입 오류를 고칠 정리를 나타내는 홀을 삽입해요. Idris는 모듈과 함수 이름에서 생성된 이름을 가진 두 개의 증명 의무(proof obligations)가 있다고 알려줘요:

*views> :m
Global holes:
        [views.parity_lemma_2,views.parity_lemma_1]

첫 번째는 다음 타입을 가져요:

*views> :p views.parity_lemma_1

---------------------------------- (views.parity_lemma_1) --------
{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))

-views.parity_lemma_1>

두 인자는 패턴 매치에서 범위에 있는 변수 j와, 잠정 정의의 오른쪽에서 준 값인 value이에요. 우리의 목표는 이 값을 사용할 수 있도록 타입을 다시 쓰는 것이에요. 프렐류드의 다음 정리를 사용해 이를 달성할 수 있어요:

plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
  S (left + right) = left + (S right)

plus의 정의를 펼치기 위해 다시 compute를 사용해야 해요:

-views.parity_lemma_1> compute


---------------------------------- (views.parity_lemma_1) --------
{hole0} : (j : Nat) -> (Parity (S (plus j (S j)))) -> Parity (S (S (plus j j)))

intros를 적용한 후:

-views.parity_lemma_1> intros

  j : Nat
  value : Parity (S (plus j (S j)))
---------------------------------- (views.parity_lemma_1) --------
{hole2} : Parity (S (S (plus j j)))

그 다음 plusSuccRightSucc 다시 쓰기 규칙을 j와 j에 대해 대칭적으로 적용해요:

-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)

  j : Nat
  value : Parity (S (plus j (S j)))
---------------------------------- (views.parity_lemma_1) --------
{hole3} : Parity (S (plus j (S j)))

sym은 다시 쓰기의 순서를 뒤집는 라이브러리에 정의된 함수예요:

sym : l = r -> r = l
sym Refl = Refl

전제에서 value를 찾는 사소한(tivial) 택틱을 사용해 이 증명을 완성할 수 있어요. 두 번째 보조 정리의 증명은 정확히 같은 방식으로 진행돼요.

이제 The with rule — matching intermediate values 절의 natToBin 함수를 프롬프트에서 테스트할 수 있어요. 숫자 42는 이진수로 101010이에요. 이진 숫자는 뒤집혀 있어요:

*views> show (natToBin 42)
"[False, True, False, True, False, True]" : String

불신의 정지 (Suspension of Disbelief)

Idris는 프로그램을 컴파일하기 전에 증명이 완성되기를 요구해요 (프롬프트에서의 평가는 증명 세부 사항 없이도 가능하지만). 때로는, 특히 프로토타이핑할 때, 이것을 하지 않는 것이 더 쉽게 느껴질 수 있어요. 프로그램에 대해 증명을 시도하기 전에 테스트하는 것이 이로울 수도 있어요 — 테스트가 오류를 찾으면, 무엇인가를 증명하는 데 시간을 낭비하지 않는 편이 낫다는 것을 알게 되니까요!

따라서 Idris는 잘못된 타입의 값을 사용할 수 있게 해주는 내장 강제 함수(coercion function)를 제공해요:

believe_me : a -> b

분명히 이것은 극도로 주의해서 사용해야 해요. 프로토타이핑할 때 유용하고, 외부 코드(어쩌면 외부 C 라이브러리)의 속성을 단언할 때도 적절할 수 있어요. 이것을 사용한 views.parity_lemma_1의 "증명"은 다음과 같아요:

views.parity_lemma_2 = proof {
    intro;
    intro;
    exact believe_me value;
}

exact 택틱은 증명에 대한 정확한 값을 제공할 수 있게 해줘요. 이 경우 우리가 준 값이 정확하다고 단언해요.

예: 이진수 (Example: Binary numbers)

앞서 Parity 뷰를 사용해 이진수로의 변환을 구현했어요. 여기서는 같은 뷰를 사용해 검증된 이진수 변환을 구현하는 방법을 보여줄게요. 이진수를 그 Nat 등가물로 인덱싱하는 것으로 시작해요. 이것은 표현(이 경우 Binary)을 의미(이 경우 Nat)와 연결하는 흔한 패턴이에요:

data Binary : Nat -> Type where
   BEnd : Binary Z
   BO : Binary n -> Binary (n + n)
   BI : Binary n -> Binary (S (n + n))

BO와 BI는 이진수를 인자로 취하고, 사실상 그것을 한 비트 왼쪽으로 시프트해 새 최하위 비트로 0 또는 1을 더해요. 인덱스 n + n 또는 S (n + n)은 이 왼쪽 시프트 후 덧셈이 숫자의 의미에 가질 결과를 진술해요. 이것은 최하위 비트가 맨 앞에 있는 표현을 만들 거예요.

이제 Nat를 이진수로 변환하는 함수는, 타입에서 결과 이진수가 원래 Nat의 충실한 표현이라고 진술할 거예요:

natToBin : (n:Nat) -> Binary n

Parity 뷰는 정의를 꽤 간단하게 만들어요 — 숫자를 반으로 나누는 것이 결국 효과적으로 오른쪽 시프트니까요 — 비록 Odd 경우에는 잠정 정의를 사용해야 하지만요:

natToBin : (n:Nat) -> Binary n
natToBin Z = BEnd
natToBin (S k) with (parity k)
   natToBin (S (j + j))     | Even  = BI (natToBin j)
   natToBin (S (S (j + j))) | Odd  ?= BO (natToBin (S j))

Odd 경우의 문제는 parity의 정의에서와 같으며, 증명도 같은 방식으로 진행돼요:

natToBin_lemma_1 = proof {
    intro;
    intro;
    rewrite sym (plusSuccRightSucc j j);
    trivial;
}

마무리하려면, 사용자로부터 정수를 읽어 이진수로 출력하는 메인 프로그램을 구현할게요.

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          print (natToBin (fromInteger (cast x)))

물론 이것이 작동하려면 Binary n에 대한 Show 구현이 필요해요:

Show (Binary n) where
    show (BO x) = show x ++ "0"
    show (BI x) = show x ++ "1"
    show BEnd = ""

출처: 문서