ㄷㅁ보다 내 뻘소리가 더 의미 있을껄?

[기괴공학도(mecheng98)]

어떤 타입의 값은
그 타입의 생성자를 주생성자로 하는
하위값들의 결합이다.
형식언어에 비유하면
타입은 시작 심볼으로
값은 문장으로
생성자는 터미널 심볼로
생각할 수 있다.
예를 들어 "
Nat ::= "s" Nat | "z".
"로 자연수를 정의할 수 있다.
그리고 항 t가 타입 T에 속하는 걸 "
t : T
"로 나타내자.
그러면 t : T이고 s : T일 때만 t = s는 식이다.
변수들 x1:T1, ..., xn:Tn와 함수 f : T1 * ... * Tn → T에 대하여 항 f(x1, ..., xn)은 타입 T에 속한다.
그리고 술어 P와 항들의 타입이 맞아야 formula가 된다.

- 희망의 등불