포스툴레이트

포스툴레이트 (Postulates)

포스툴레이트(postulate)는 어떤 타입의 원소에 대한 선언이면서 동반되는 정의는 없는 선언이에요. 포스툴레이트를 사용하면 원소 자체의 정의를 실제로 주지 않고도 타입에 원소를 도입할 수 있어요.

포스툴레이트 선언의 일반적인 형태는 다음과 같아요:

postulate
    c11 ... c1i : <Type>
    ...
    cn1 ... cnj : <Type>

포스툴레이트 블록은 instance와 private 선언을 포함할 수 있어요.

기본 포스툴레이트 블록의 예:

postulate
  A B    : Set
  a      : A
  b      : B
  _=AB=_ : A → B → Set
  a==b   : a =AB= b

포스툴레이트를 도입하는 것은 일반적으로 권장되지 않아요. 포스툴레이트를 도입하면 전체 개발의 일관성(consistency)이 위험해지는데, 그 이유는 빈 집합에 원소를 도입하는 것을 막을 아무것도 없기 때문이에요.

data False : Set where

postulate bottom : False

포스툴레이트는 실수로 인한 불일치를 막기 위해 Safe Agda(--safe 옵션)에서 금지돼요.

가정과 작업하는 더 바람직한 방법은 우리가 필요한 원소로 매개변수화된 모듈을 정의하는 것이에요:

module Absurd (bt : False) where

  -- ...

module M (A B : Set) (a : A) (b : B)
         (_=AB=_ : A → B → Set) (a==b : a =AB= b) where

  -- ...

Float, Char와 같은 일부 빌트인은 포스툴레이트로 도입된 다음 해당 {-# BUILTIN ... #-} 프래그마에 의해 의미가 부여돼요.

포스툴레이트는 선언이므로 임의의 선언이 허용되는 위치, 예를 들어 where 블록에 나타날 수 있어요:

module PostulateInWhere where

  my-theorem : (A : Set) → A
  my-theorem A = I-prove-this-later
    where
      postulate I-prove-this-later : _