PL wiki

단순 타입 λ-계산

  • λ-계산
  • 연역 체계

단순 타입 λ-계산(simply typed λ-calculus, STLC)는 함수 타입, 곱 타입, 합 타입, 자연수 타입 등을 허용하는 간단한 타입 체계를 갖춘 λ-계산이다. 커리-하워드 대응 관점에서 단순 타입 λ-계산은 자연 연역 방식 명제 논리 체계의 일종으로 볼 수 있다.

추상 문법

\[ \newcommand{\fst}[0] {\mathbf{fst}} \newcommand{\snd}[0] {\mathbf{snd}} \newcommand{\inl}[0] {\mathbf{inl}} \newcommand{\inr}[0] {\mathbf{inr}} \newcommand{\case}[0] {\mathbf{case}} \newcommand{\tt}[0] {\mathbf{tt}} \newcommand{\absurd}[0] {\mathbf{absurd}} \newcommand{\1}[0] {\mathbf{1}} \newcommand{\0}[0] {\mathbf{0}} \begin{array}{ll} L, M, N &::= x \mid λx. M \mid M \ N \mid \langle M , N \rangle \mid \fst(M) \mid \snd(M) \mid \inl(M) \mid \inr(M) \mid \case(L, x.M, y.N) \mid \tt \mid \absurd(M) \\ A, B, C &::= A \to B \mid A \times B \mid A + B \mid \1 \mid \0 \\ \Gamma &::= \cdot \mid \Gamma , x : A \end{array} \]

타입 시스템

변수

\[ \begin{prooftree} \AXC{ $\Gamma \ni x : A$ } \UIC{ $\Gamma \vdash x : A$ } \end{prooftree} \]

함수 타입

\[ \begin{prooftree} \AXC{ $\Gamma , x : A \vdash M : B$ } \RL{ ${\to}I$ } \UIC{ $\Gamma \vdash \lambda x. M : A \to B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M : A \to B$ } \AXC{ $\Gamma \vdash N : A$ } \RL{ ${\to}E$ } \BIC{ $\Gamma \vdash M \ N : B$ } \end{prooftree} \]

곱 타입

\[ \begin{prooftree} \AXC{ $\Gamma \vdash M : A$ } \AXC{ $\Gamma \vdash N : B$ } \RL{ ${\times}I$ } \BIC{ $\Gamma \vdash \langle M , N \rangle : A \times B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M : A \times B$ } \RL{ ${\times}E_1$ } \UIC{ $\Gamma \vdash \fst(M) : A$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M : A \times B$ } \RL{ ${\times}E_2$ } \UIC{ $\Gamma \vdash \snd(M) : B$ } \end{prooftree} \]

합 타입

\[ \begin{prooftree} \AXC{ $\Gamma \vdash M : A$ } \RL{ ${+}I_1$ } \UIC{ $\Gamma \vdash \inl(M) : A+B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M : B$ } \RL{ ${+}I_2$ } \UIC{ $\Gamma \vdash \inr(M) : A+B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash L : A+B$ } \AXC{ $\Gamma, x:A \vdash M : C$ } \AXC{ $\Gamma, y:B \vdash N : C$ } \RL{ ${+}E$ } \TIC{ $\Gamma \vdash \case(L,x.M,y.N) : C$ } \end{prooftree} \]

\(\1\) 타입

\[ \begin{prooftree} \AXC{} \RL{ $\1 I$ } \UIC{ $\Gamma \vdash \tt : \1$ } \end{prooftree} \]

\(\0\) 타입

\[ \begin{prooftree} \AXC{ $\Gamma \vdash M : \0$ } \RL{ $\0 E$ } \UIC{ $\Gamma \vdash \absurd(M) : C$ } \end{prooftree} \]

실행 의미론

Small-step semantics (call-by-value, left-to-right)

값 규칙

\[ \newcommand{\val}[1] {#1 \ \mathrm{value}} \begin{prooftree} \AXC{} \UIC{ $\val{\lambda x. M}$ } \end{prooftree} \quad \begin{prooftree} \AXC{} \UIC{ $\val{\langle M, N \rangle}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\val{M}$ } \UIC{ $\val{\inl(M)}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\val{M}$ } \UIC{ $\val{\inr(M)}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ } \UIC{ $\val{\tt}$ } \end{prooftree} \]

축약 규칙

\[ \begin{prooftree} \AXC{ $\val{N}$ } \UIC{ $(\lambda x. M) \ N \longrightarrow M [N/x] $ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\fst(\langle M , N \rangle) \longrightarrow M $ } \end{prooftree} \quad \begin{prooftree} \AXC{} \UIC{ $\snd(\langle M , N \rangle) \longrightarrow N $ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\val{L}$ } \UIC{ $\case(\inl(L), x.M, y.N) \longrightarrow M[L/x]$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\val{L}$ } \UIC{ $\case(\inr(L), x.M, y.N) \longrightarrow N[L/y]$ } \end{prooftree} \]

구조 규칙

\[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $M \ N \longrightarrow M' \ N$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\val{M}$ } \AXC{ $N \longrightarrow N'$ } \BIC{ $M \ N \longrightarrow M \ N'$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\fst(M) \longrightarrow \fst(M')$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\snd(M) \longrightarrow \snd(M')$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\inl(M) \longrightarrow \inl(M')$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\inr(M) \longrightarrow \inr(M')$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $L \longrightarrow L'$ } \UIC{ $\case(L,x.M,y.N) \longrightarrow \case(L',x.M,y.N)$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\absurd(M) \longrightarrow \absurd(M')$ } \end{prooftree} \]

Small-step semantics (full β-reduction)

축약 규칙

\[ \begin{prooftree} \AXC{} \UIC{ $(\lambda x. M) \ N \longrightarrow M [N/x] $ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\fst(\langle M , N \rangle) \longrightarrow M $ } \end{prooftree} \quad \begin{prooftree} \AXC{} \UIC{ $\snd(\langle M , N \rangle) \longrightarrow N $ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $$ } \UIC{ $\case(\inl(L), x.M, y.N) \longrightarrow M[L/x]$ } \end{prooftree} \quad \begin{prooftree} \AXC{ } \UIC{ $\case(\inr(L), x.M, y.N) \longrightarrow N[L/y]$ } \end{prooftree} \]

구조 규칙

\[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\lambda x. M \longrightarrow \lambda x. M'$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $M \ N \longrightarrow M' \ N$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $N \longrightarrow N'$ } \UIC{ $M \ N \longrightarrow M \ N'$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\langle M , N \rangle \longrightarrow \langle M' , N \rangle$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $N \longrightarrow N'$ } \UIC{ $\langle M, N \rangle \longrightarrow \langle M , N' \rangle$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\fst(M) \longrightarrow \fst(M')$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\snd(M) \longrightarrow \snd(M')$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\inl(M) \longrightarrow \inl(M')$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\inr(M) \longrightarrow \inr(M')$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $L \longrightarrow L'$ } \UIC{ $\case(L,x.M,y.N) \longrightarrow \case(L',x.M,y.N)$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\case(L,x.M,y.N) \longrightarrow \case(L,x.M',y.N)$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $N \longrightarrow N'$ } \UIC{ $\case(L,x.M,y.N) \longrightarrow \case(L,x.M,y.N')$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $M \longrightarrow M'$ } \UIC{ $\absurd(M) \longrightarrow \absurd(M')$ } \end{prooftree} \]

정규형

\[ \begin{prooftree} \AXC{ $\Gamma \ni x : A$ } \UIC{ $\Gamma \vdash x \Rightarrow A$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M \Rightarrow A$ } \UIC{ $\Gamma \vdash M \Leftarrow A$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\Gamma, x:A \vdash M \Leftarrow B$ } \UIC{ $\Gamma \vdash \lambda x. M \Leftarrow A \to B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M \Rightarrow A \to B$ } \AXC{ $\Gamma \vdash N \Leftarrow A$ } \BIC{ $\Gamma \vdash M \ N \Rightarrow B$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\Gamma \vdash M \Leftarrow A$ } \AXC{ $\Gamma \vdash N \Leftarrow B$ } \BIC{ $\Gamma \vdash \langle M, N \rangle \Leftarrow A \times B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M \Rightarrow A \times B$ } \UIC{ $\Gamma \vdash \fst(M) \Rightarrow A$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M \Rightarrow A \times B$ } \UIC{ $\Gamma \vdash \snd(M) \Rightarrow B$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\Gamma \vdash M \Leftarrow A$ } \UIC{ $\Gamma \vdash \inl(M) \Leftarrow A + B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M \Leftarrow A$ } \UIC{ $\Gamma \vdash \inr(M) \Leftarrow A + B$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash L \Rightarrow A + B$ } \AXC{ $\Gamma, x:A \vdash M \Leftarrow C$ } \AXC{ $\Gamma, y:B \vdash N \Leftarrow C$ } \TIC{ $\Gamma \vdash \case(L,x.M,y.N) \Rightarrow C$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\Gamma \vdash \tt \Leftarrow \1$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\Gamma \vdash M \Rightarrow \0$ } \UIC{ $\Gamma \vdash \absurd(M) \Rightarrow C $ } \end{prooftree} \]

Small-step semantics (full β-reduction with commuting reduction)

교환 규칙

full β-reduction에 다음의 교환 규칙을 추가한다. \[ \begin{prooftree} \AXC{} \UIC{ $\case(L, x.M, y.N) \ N' \longrightarrow \case(L, x. M \ N', y. N \ N')$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\fst(\case(L, x.M, y.N)) \longrightarrow \case(L, x. \fst(M), y. \fst(N))$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\snd(\case(L, x.M, y.N)) \longrightarrow \case(L, x. \snd(M), y. \snd(N))$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\case(\case(L, x.M, y.N), x'.M', y'.N') \longrightarrow \case(L, x. \case(M, x'.M', y'.N'), y. \case(N, x'.M', y'.N'))$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\absurd(\case(L, x.M, y.N)) \longrightarrow \case(L, x. \absurd(M), y. \absurd(N))$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\absurd(M) \ N' \longrightarrow \absurd(M)$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\fst(\absurd(M)) \longrightarrow \absurd(M)$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\snd(\absurd(M)) \longrightarrow \absurd(M)$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\case(\absurd(L), x'.M', y'.N') \longrightarrow \absurd(L)$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{} \UIC{ $\absurd(\absurd(M)) \longrightarrow \absurd(M)$ } \end{prooftree} \]

정규형

\(\case\)와 \(\absurd\)에 대한 규칙을 다음과 같이 바꾼다. \[ \begin{prooftree} \AXC{ $\Gamma \vdash L \Rightarrow A + B$ } \AXC{ $\Gamma, x:A \vdash M \Leftarrow C$ } \AXC{ $\Gamma, y:B \vdash N \Leftarrow C$ } \TIC{ $\Gamma \vdash \case(L,x.M,y.N) \Leftarrow C$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\Gamma \vdash M \Rightarrow \0$ } \UIC{ $\Gamma \vdash \absurd(M) \Leftarrow C $ } \end{prooftree} \]