:opt no-lint
(주교재 관련 내용: 8.7, 16.7, 17)
문법
$\begin{array}{lll} n \in \textsf{Int} & \\ e \in \textsf{Expr} &::=& n \\ &\quad\mid& e \;✚\; e \end{array}$
계산 규칙 ($e \Downarrow n$)
$\displaystyle \frac{~~}{n \Downarrow n} \qquad \frac{e_1 \Downarrow n_1 \quad e_2 \Downarrow n_2}{ e_1 \,✚\, e_2 \Downarrow n_1+n_2}$
추론규칙의 형태로 나타낸 계산규칙
프로그램의 의미를 나타내는 operational semantics
-- Abstract Syntax Tree를 나타내는 하스켈 데이타 타입 Expr 정의
data Expr = Val Int -- n
| Add Expr Expr -- e1 + e2
deriving Show
(Add (Add (Val 2) (Val 3)) (Val 4)) -- (2 + 3) + 4
Add (Add (Val 2) (Val 3)) (Val 4)
:type (Add (Add (Val 2) (Val 3)) (Val 4))
eval :: Expr -> Int
eval (Val n) = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Add (Val 2) (Val 3))
eval (Val 4)
5
4
eval (Add (Add (Val 2) (Val 3)) (Add (Val 4) (Val 5))) -- (2 + 3) + (4 + 5)
14
eval $ (Val 2 `Add` Val 3) `Add` (Val 4 `Add` Val 5) -- (2 + 3) + (4 + 5)
14
위에서 살펴본 가장 간단한 인터프리터는 분명 맞는 결과를 계산한다. 그런데 잘 생각해 보면 계산 우리가 앞에서 살펴본 계산규칙은 계산 순서가 정해져 있지 않아 여러 가지 순서로 계산이 가능하다. 물론 덧셈의 결합법칙이라는 성질에 의해 계산 순서에 관계없이 값은 같게 나온다.
하지만 내가 정의한 언어에서 계산 순서를 정하고 싶다면 어떨까? 예를 들어 어떤 언어는 함수를 호출할 때 왼쪽에 있는 인자부터 먼저 계산한다던가 또 다른 언어는 오른쪽에 있는 인자부터 계산한다던가 하는 순서를 정해 놓기도 하고, 또 어떤 언어는 그런 순서는 정의되어 있지 않고 언어를 구현하는 사람이 (즉 인터프리터나 컴파일러 등을 만드는 개발자가) 자유롭게 해도 무방하다고 약속하는 경우도 있다.
정수 덧셈 언어를 실행할 때 계산 순서를 분명히 정하려면 계산 규칙을 조금 다르게 정해야 한다.
$\displaystyle \frac{~~}{n \Downarrow_L n} \qquad\qquad \frac{}{ n_1 ✚\, n_2 \Downarrow_L n_1+n_2} $
$\displaystyle \frac{e_2 \Downarrow_L n_2}{ n_1 ✚\, e_2 \Downarrow_L n_1+n_2 }~(e_2\notin\textsf{Int}) \qquad \frac{e_1 \Downarrow_L n_1 \quad n_1 ✚\, e_2 \Downarrow_L n}{ e_1 ✚\, e_2 \Downarrow_L n}~(e_1\notin\textsf{Int}) $
만일 덧셈의 왼쪽부터 먼저 항상 계산하도록 하려면 아래와 계산 규칙에 따라 위의 eval
과는 조금 다른 인터프리터를 정의해야 된다.
이렇게 바뀐 계산규칙에 따라 evalL
이라는 함수로 인터프리터를 작성해 보자.
evalL (Val n) = n
evalL (Add (Val n1) (Val n2)) = n1 + n2
evalL (Add (Val n1) e2) = n1 + n2
where n2 = evalL e2
evalL (Add e1 e2) = evalL (Add (Val n1) e2)
where n1 = evalL e1
{- -- 지역변수를 앞쪽에 정의하려면 let ... in ... 식을 쓰면 된다
evalL (Add (Val n1) e2) = let n2 = eval e2
in n1 + n2
evalL (Add e1 e2) = let n1 = eval e1
in evalL (Add (Val n1) e2)
-}
evalL (Add (Add (Val 2) (Val 3)) (Add (Val 4) (Val 5))) -- (2 + 3) + (4 + 5)
14
evalL (Add (Add (Val 2) (Val 3)) (Add (Val 4) (Val 5)))
evalL (Add (Val 2) (Val 3)) --> 5 -- e1을 n1으로 먼저 계산
-->
evalL (Add (Val 5) (Add (Val 4) (Val 5)))
evalL (Add (Val 4) (Val 5)) --> 9 -- 왼쪽이 이미 정수 형태이므로 e2를 n2로 계산
-->
14
연습문제 03-01
연산자의 오른쪽부터 먼저 계산하는 evalR
을 정의하라.
$\displaystyle \frac{~~}{n \Downarrow_R n} \qquad\qquad \frac{}{ n_1 ✚\, n_2 \Downarrow_R n_1+n_2} $
$\displaystyle \frac{e_1 \Downarrow_R n_2}{ e_1 ✚\, n_2 \Downarrow_R n_1+n_2 }~(e_1\notin\mathsf{Int}) \qquad \frac{e_2 \Downarrow_R n_2 \quad e_1 ✚\, n_2 \Downarrow_R n}{ e_1 ✚\, e_2 \Downarrow_R n}~(e_2\notin\mathsf{Int}) $
-- evalR :: Expr -> Int
(작은걸음 동작방식 의미론)
지금까지 살펴본 프로그래밍 언어의 의미를 기술하는 방식을 큰걸음 동작방식 의미론(big-step operational semantics)라고 한다.
이는 인터프리터를 재귀함수로 작성하는 데 있어 가장 직관적이고 자연스러운 의미론(semantics)이다.
eval
, evalL
, evalR
같은 함수를 식에 대해 호출하면 최종적으로 어떤 값이 계산된다는 동작 방식으로 기술되어 있기 때문이다.
그런데 우리가 좀전에 앞에서 evalL
이 어떻게 동작하는지를 이해하기 위해 화살표를 그려 가며 생각해 본 메모를 살펴보면
한번에 큰 걸음으로 전체 식에서 최종 정수 결과값을 바로 뚝딱 하고 생각하는 것이 아니라 계산 과정에 어떤 단계를 거치는지도
생각하는 과정에서 나타나고 있다. 이런 중간과정의 각 단계가 어떠한지 드러내는 방식으로 프로그래밍 언어의 의미를 기술할 수도 있는데
이를 작은걸음 동작방식 의미론(small-step operational semantics)라고 한다.
큰걸음이나 작은걸음 같은 용어는 동작방식 의미론 중에서 세부적인 종류이므로
그냥 줄여서 큰걸음 의미론(big-step semantics), 작은걸음 의미론(small-step semantics)라고도 부른다.
사실 우리가 초등학교 중학교부터 식을 줄여나갈 때도 작은 걸음 의미론과 비슷한 방식으로 해왔었다.
(2 + 3) + (4 + 5) = 5 + (4 + 5) = 5 + 9 = 14
(2 + 3) + (4 + 5) = (2 + 3) + 9 = 5 + 9 = 14
위의 식을 줄여나가는 과정에서 = 대신에 방향성이 있는 화살표 같은 기호로 주로 작은걸음 의미론을 나타냅니다.
eval
에 해당하는 작은걸음 의미론의 계산 규칙($e \longrightarrow e'$)은 다음과 같다.
$\displaystyle \frac{~~}{n_1 ✚\, n_2 \longrightarrow n_1+n_2} \qquad \frac{e_1 \longrightarrow e_1'}{e_1 ✚\, e_2 \longrightarrow e_1' ✚\,e_2} \qquad \frac{e_2 \longrightarrow e_2'}{e_1 ✚\, e_2 \longrightarrow e_1 ✚\,e_2'} $
연습문제 03-02
식 (2 + 3) + (4 + 5)
를 작은걸음 의미론으로 여러 단계에 걸쳐 계산을 진행하려 한다.
(1) 첫 번째 단계의 한 걸음을 규칙을 따라 유도하라. 참고로 하나 이상의 경우가 있으니 모든 가능한 경우를 살펴보라.
------------- 첫번째 규칙
2 + 3 --> 5
------------------------------------ 두번째 규칙
(2 + 3) + (4 + 5) --> 5 + (4 + 5)
-------------- 첫번째 규칙
4 + 5 --> 9
------------------------------------ 세번째 규칙
(2 + 3) + (4 + 5) --> (2 + 3) + 9
(2) 첫 번째 단계의 각각의 결과로부터 그 다음 두 번째 단계의 한 걸음을 규칙을 따라 유도하라.
------------- 첫번째 규칙
4 + 5 --> 9
------------------------ 세번째 규칙
5 + (4 + 5) --> 5 + 9
------------- 첫번째 규칙
2 + 3 --> 5
------------------------ 두번째 규칙
(2 + 3) + 9 --> 5 + 9
evalL
에 해당하는 작은걸음 의미론의 계산 규칙($e \longrightarrow_L e'$)은 다음과 같다.
$\displaystyle \frac{~~}{n_1 ✚\, n_2 \longrightarrow_L n_1+n_2} \qquad \frac{e_1 \longrightarrow_L e_1'}{e_1 ✚\, e_2 \longrightarrow_L e_1'✚\,e_2} \qquad \frac{e_2 \longrightarrow_L e_2'}{n_1 ✚\, e_2 \longrightarrow_L n_1✚\,e_2'} $
큰걸음 의미론에서 $e \Downarrow n$는 작은걸음 의미론으로는 여러 단계에 걸친 $e \longrightarrow \cdots \longrightarrow n$에 해당한다.
stepL :: Expr -> Expr
stepL (Add (Val n1) (Val n2)) = Val (n1 + n2)
stepL (Add (Val n1) e2) = Add (Val n1) e2' where e2' = stepL e2
stepL (Add e1 e2) = Add e1' e2 where e1' = stepL e1
stepL (Val n) = error $ show (Val n) ++ " cannot stepL"
stepL (Add (Add (Val 2) (Val 3)) (Add (Val 4) (Val 5)))
stepL it
stepL it
-- stepL it -- error
Add (Val 5) (Add (Val 4) (Val 5))
Add (Val 5) (Val 9)
Val 14
연습문제 03-03
식 (2 + 3) + (4 + 5)
를 작은걸음 의미론 $\longrightarrow_L$로 여러 단계에 걸쳐 계산을 진행하려 한다.
(1) 첫 번째 단계의 한 걸음을 규칙을 따라 유도하라. 딱 한 가지 경우밖에 없을 것이다.
-------------- 첫번째 규칙
2 + 3 -->L 5
------------------------------------ 두번째 규칙
(2 + 3) + (4 + 5) -->L 5 + (4 + 5)
(2) 첫 번째 단계의 결과로부터 그 다음 두 번째 단계의 한 걸음을 규칙을 따라 유도하라
-------------- 첫번째 규칙
4 + 5 -->L 9
------------------------ 세번째 규칙
5 + (4 + 5) -->L 5 + 9
연습문제 03-04
위에서 정의한 stepL
을 반복적으로 적용해
최종적으로는 evalL
과 같은 결과를 계산하는 함수 runL
을 정의하라.
-- runL :: Expr -> Int
참고로, 이 수업에서 프로그래밍 언어의 의미를 기술할 때 사용하는 방법은 대부분 동작방식 의미론(operational semantics)에 속하지만 이와는 또 다른 방식으로 프로그래밍 언어의 의미를 기술하기도 한다. 어떤 프로그래밍 언어로 작성된 가능한 모든 프로그램의 의미를 포괄하는 수학적 대상(예를 들면 집합, 부분순서집합, 격자 등등)을 설정하여 각각의 프로그램이 그 대상에 속하는 개체를 지시하도록 의미를 부여하는 지시적 의미론(denotational semantcis)과 프로그램이 만족해야 할 성질을 논리식으로 도출하여 기술하는 공리적 의미론(axiomatic semantics)이 지금까지 이 수업에서 우리가 접해 본 동작방식 의미론(operational semantics)과 함께 가장 대표적인 프로그래밍 언어 의미 기술 방식이다. 좀더 이론적인 것에 관심이 있는 학생들이라면 이런 것들이 무엇인지 조사해 보는 것도 좋겠다.
여기서 수업에서 직접적으로 다루지 않는 이런 이론적인 용어까지 굳이 소개하고 넘어가는 이유는 지시적(denotational)이니 공리적(axiomatic)이니 하는 이런 용어들이 철학 및 논리학에서 온 용어이기 때문이다. 프로그래밍 언어를 포함해 컴퓨터 과학/공학 분야에는 이런 철학이나 논리학에서 넘어온 용어들이 의외로 꽤 많다. 이공계가 인문학적 소양이 부족하다느니 하는데 교양 수업에서 개론적인 것을 듣는 것도 좋지만 컴퓨터 과학/공학을 정말 기초부터 깊게 용어 하나하나까지 유래를 따져 보며 공부한다면 철학과 논리학 분야에 접근하는 데도 도움이 된다. 또 반대로 인문학에서 철학과 논리학을 정말 제대로 공부한 사람이라면 컴퓨터 분야에서 이런 용어를 접했을 때 전공자들보다 깊이 있는 통찰력을 가지는 경우도 있을 수 있다.