Account: please sign in
AA

변수 하나와 표현식 하나에 적용되어 표현식 하나로 환산되되, 표현식 속에 등장하는 인자 변수가 특정한 의미로 통용됨을 나타내는 연산자를 (변수) 바인딩 연산자variable-binding operators라고 합니다. 개념적으로 간단히 말하자면, 변수가 특별한 의미를 가지는 스코프scope를 지정해주는 연산자들입니다.

우리가 이미 흔히 알고있는 바인딩 연산자에는 ∀, ∃ 등이 있습니다. 만일 x가 변수이고 E가 표현식일 때, "∀x, E"라는 표현식은

  • "모든 x에 대해서"라는 의미를 부여함과 동시에
  • 표현식 E 속에 (새롭게 달리 바인딩되지 않고 그냥) 등장하는 x들은 바로 그 ('모든'이라고 말했던) x를 가리킴을 알리는 것입니다.

바인딩 연산자는 관례적으로 중위 형태("x∀E" 형태)가 아닌 특별한 형태로 사용합니다: 맨 앞에 바인딩 연산자가 오고, 그 뒤에 '묶일' 변수가 표시되며, 그 뒤에 그 변수의 소속을 (∈이나 : 기호와 더불어) 표시해도 되고 안해도 되고 (혹은, 별다른 기호 없이 소속만 윗첨자로 쓰고), 그 뒤에 구획문자(delimiter)가 (거의 반드시) 나오고, 그 뒤에 표현식이 쭉 뒤따르는 형태입니다.

  • BindOp Var [ ( Set | : Type) ] [ Delimiter ] Expression
    BindOp Var Type [ Delimiter ] Expression

예를 들어, 다음과 같은 표현식들은 전부 올바른 바인딩 연산자 사용 예입니다:

  • ∀x, 0 ≤ x
  • ∀x∈N, 0 ≤ x

  • ∀x:N, 0 ≤ x

  • ∀xN, 0 ≤ x

소속을 어떻게 표시하느냐는 주위 문맥과 설정에 달렸습니다.

  • 대체로 집합론 설정 하에서라면 (Z 등) 소속 기호로 ''을 쓰고, 타입 이론 설정 하에서라면 (Coq 등) 소속 기호로 ':'를 씁니다.

  • 소속을 윗첨자로 표시하는 경우는 여기저기서 종종 보이지만, 특히 typed lambda-calculus에서는 소속을 거의 언제나 윗첨자로만 표시합니다: λxN.(x+1)

구획문자는 각 바인딩 연산자마다 관례적으로 자주 함께 쓰이는 기호가 몇 가지씩 있습니다:

  • 논리적 바인딩들(∀, ∃, ∃1 등)의 경우, 구획 문자로는 여러가지가 쓰입니다. 중요한 것은, 한 시리즈의 문서들 내에서 일관성 있게 정해서 사용하기만 하면 된다는 것입니다. 현재 주요 관례들은:

    • Z (zed)라는 정형 명세 언어의 경우, 아주 작지도 너무 크지도 않으며 까맣게 채워지고 높이가 문장의 가운데인 둥근 점(disc, dot, black circle)이 쓰입니다: ∀x∈N ● 0 ≤ x

    • Coq의 경우 쉼표가 쓰입니다: ∀x:nat, 0 ≤ x
    • 조금 고전적인 텍스트의 경우 구획문자를 생략하는 경우도 있습니다만, 정형적 파싱을 고려할 때 그다지 바람직하진 않아 보입니다: ∀x P(x)
  • 추후 보게될 람다 바인딩의 경우, 구획문자로는 거의 100% 마침표(.)만 쓰입니다: λx.(x+1)

  • 자연어로 기술된 수학 문서나 함수형 프로그래밍 언어에 등장하는 let 바인딩의 경우, 구획문자로 대부분 "in"이라는 문자열을 사용합니다 (아예 "let-in 구문"이라고 부르기도 합니다):
    let x = 3 in f(x) + g(x2)

바인딩 연산자의 결합 특성은 어떨까요? 다시 말해서, 바인딩 연산자의 바인딩 스코프는 정확히 어디부터 어디까지일까요? 정답은, 바인딩 연산자의 바인딩 스코프는

  • 구획문자 직후부터 시작되며,
  • 바인딩 연산자 자체보다 앞서서 열렸던 괄호가
    • (만일 있었다만) 그 괄호가 닫히는 곳에서 끝나고
    • (만일 없었다면) 표현식이 끝나는 곳에서 끝난다.

입니다.

또다른 형태의 바인딩 연산자로는 함수 정의가 있습니다. 잘 알고계실 C 언어의 함수 정의

   1 int
   2 foo(int x) {
   3     return (x + 1);
   4 }

에서, 함수 이름이 바인딩 연산자가 되고 x가 '묶인' 변수,{부터 }까지의 함수 정의 본체가 x의 바인딩 스코프가 됩니다.