과제 4. 연산적 의미구조(operational semantics)를 사용해 동적 의미구조(dynamic semantics) 구현하기

제출방법 : 작성한 프로젝트를 ‘{학번}’라는 이름으로 저장한 후 압축하여 Uclass 과제 게시판에 업로드해주세요. 채점은 스크립트로 자동으로 이루어지기에 폴더 이름이 잘못되어서 채점되지 못하면 0점을 받게 됩니다.
- 예시: 학번이 202448015인 학생은 다음과 같은 프로젝트를 202448015.zip으로 압축해서 제출해야 합니다.
```
  202448015
  ├── dune-project
  ├── src
  │   ├── ast.ml
  │   ├── dune
  │   ├── interpreter.ml
  │   ├── lexer.mll
  │   └── parser.mly
  └── test
      ├── dune
      └── main.ml 
```
제출기한 : 5월 15일 목요일 11:59pm

과제 진행 시 어려운 점이 있으면 Ed Discussion 게시판을 이용해 질문하세요. 게시판을 통해 하기 어려운 질문이라면 아래 TA 이메일을 통해 문의하시기 바랍니다.

TA 이메일: seongminkim16@gmail.com

지난 두 개의 과제를 통해서 주어진 소스 코드를 AST로 변환하는 작업을 수행했습니다. 이제 이 AST를 평가(evaluation)할 수 있도록 동적 의미구조를 구현하도록 하겠습니다. 평가란 AST가 최종적인 값(value)이 될 때까지 계속해서 단순화하는 과정입니다. 다시 말해, 평가는 언어의 동적 의미론을 구현하는 것입니다. 우리는 이번 과제에서 연산적 의미구조를 활용해서 동적 의미구조를 기술하도록 하겠습니다.

큰 단계 평가 vs. 작은 단계 평가 (Big-step vs. Small-step Evaluation)

평가를 수학적인 관계(mathematical relation)를 사용하여 정의할 것입니다. 평가를 위해 세 가지 관계를 정의할 것입니다:

첫 번째 관계인 →는 프로그램이 단일 실행 단계(one single step of execution)를 어떻게 수행하는지를 나타냅니다.
두 번째 관계인 →*는 →의 반사적 전이 폐쇄(reflexive transitive closure)이며, 프로그램이 여러 실행 단계(multiple steps of execution)를 어떻게 수행하는지를 나타냅니다.
세 번째 관계인 ==>는 단일 단계의 모든 세부 사항을 추상화(abstracts away)하고, 프로그램이 어떻게 값(value)으로 직접 축약(reduces directly)되는지를 나타냅니다.

이러한 관계들을 사용하여 평가를 정의하는 방식을 연산적 의미론(operational semantics)이라고 합니다. 왜냐하면 이 관계들을 사용하여 기계가 프로그램을 평가할 때 어떻게 동작(operates)하는지를 명시하기 때문입니다.

조작적 의미론은 평가를 정의하는 두 가지 하위 방식, 즉 작은 단계 의미론(small-step semantics)과 큰 단계 의미론(big-step semantics)으로 더 나눌 수 있습니다.

첫 번째 관계 →는 개별적인 작은 단계(individual small steps)로 실행을 나타내므로 작은 단계 방식(small-step style)에 해당합니다.
세 번째 관계 ==>는 표현식에서 값으로 직접 이어지는 큰 단계(big step)로 실행을 나타내므로 큰 단계 방식(big-step style)에 해당합니다.
두 번째 관계 →*는 이 두 방식을 혼합합니다.

큰 단계와 작은 단계의 관계 (Relating Big and Small Steps)

모든 표현식(expression) e와 값(value) v에 대해, e -->* v 가 성립하는 것은 e ==> v 가 성립하는 것과 필요충분조건(if and only if)입니다.

다시 말해, 어떤 표현식이 여러 작은 단계를 거쳐 결국 값에 도달한다면 (예: e --> e1 --> .... --> en --> v), 이는 e ==> v 가 성립해야 함을 의미합니다. 따라서 큰 단계 관계(==>)는 작은 단계 관계(-->*)의 충실한 추상화(faithful abstraction)라고 할 수 있습니다. 즉, 모든 중간 단계(intermediate steps)를 생략한 것입니다.

왜 큰 단계와 작은 단계라는 두 가지 다른 방식을 사용할까요? 각 방식은 특정 상황에서 다른 방식보다 사용하기 조금 더 쉬울 때가 있으므로, 두 가지 모두를 우리의 도구함에 갖추는 것이 도움이 됩니다.

작은 단계 의미론(small-step semantics)은 복잡한 언어 기능(complicated language features)을 모델링(modeling)할 때 다루기 더 쉬운 경향이 있습니다.
큰 단계 의미론(big-step semantics)은 인터프리터(interpreter)가 실제로 구현되는 방식과 더 유사한 경향이 있습니다.

hw3에 대한 작은 단계 평가 규칙 (Small-step Relation)

먼저 작은 단계 평가를 정의하는 것부터 시작하겠습니다. 즉, 표현식이 한 번에 단일 단계를 어떻게 수행하는지를 나타내는 관계 →를 정의하겠습니다.

hw3의 문법을 다시 한 번 확인하겠습니다.

prog ::= e
e ::= x
    | i
    | b
    | e1 bop e2
    | if e1 then e2 else e3
    | let x = e1 in e2
bop ::= + | - | * | / | <=
x ::= <identifiers>
i ::= <integers>
b ::= true | false

표현식의 평가는 표현식이 값일때 완료됩니다. hw3의 경우 값을 정수와 불린으로 정의합니다. 즉, 값은 정수 상수(integer constant) 또는 불린 상수(Boolean constant)입니다.

v ::= i | b

hw3 표현식이 가질 수 있는 각 문법 형태(syntactic forms)에 대해, 이제 몇 가지 평가 규칙(evaluation rules)을 정의할 것입니다. 이 규칙들은 → 관계에 대한 귀납적 정의(inductive definition)를 구성합니다. 각 규칙은 e → e' 형태를 가지며, 이는 e가 e'로 단일 단계를 진행함을 의미합니다.

상수 (Constants)

정수(integer)와 불리언(Boolean) 상수는 이미 값(value)이므로, 더 이상 단계를 진행할 수 없습니다. 이것이 처음에는 이상하게 보일 수 있지만, 우리는 0번 이상의 단계를 허용하는 -->* 관계도 정의할 예정임을 기억하십시오. 반면, --> 관계는 정확히 한 단계만을 나타냅니다.

기술적으로 이를 달성하기 위해 우리가 할 일은, 어떤 표현식 e에 대해 i --> e 또는 b --> e 형태의 규칙을 작성하지 않는 것뿐입니다. 따라서 사실상 우리는 이미 이 부분을 완료한 셈입니다. 아직 아무런 규칙도 정의하지 않았기 때문입니다.

이제 e -/->라는 새로운 표기법(notation)을 도입합시다. 이는 화살표(-->)에 슬래시(/)를 그은 모양으로, e --> e 를 만족하는 e'가 존재하지 않음을 의미합니다. 즉, e가 더 이상 단계를 진행할 수 없다는 뜻입니다.

이 표기법을 사용하면 다음과 같이 쓸 수 있습니다:

i -/->
b -/->
-> 관계 정의의 엄밀한 일부는 아니지만, 이러한 명제(propositions)들은 상수가 단계를 진행하지 않는다는 것을 기억하는 데 도움이 됩니다.

사실, 더 일반적으로 모든 값(value) v에 대해 v -/->가 성립한다라고 쓸 수 있습니다.

이항 연산자 (Binary Operators)

이항 연산자 적용(binary operator application) e1 bop e2은 두 개의 하위 표현식(subexpressions) e1과 e2를 가집니다. 이는 표현식을 평가하는 방식에 대한 몇 가지 선택지를 제시합니다:

왼쪽 피연산자(left-hand side) e1을 먼저 평가한 다음, 오른쪽 피연산자(right-hand side) e2를 평가하고, 그 후에 연산자를 적용할 수 있습니다.
또는 오른쪽 피연산자를 먼저, 그 다음 왼쪽 피연산자를 평가할 수도 있습니다.
또는 평가를 번갈아 수행하여(interleave), e1의 한 단계, 그 다음 e2의 한 단계, 다시 e1의 한 단계, e2의 한 단계 등을 수행할 수도 있습니다.
어쩌면 연산자가 단락(short-circuit) 연산자일 수도 있는데, 이 경우 하위 표현식 중 하나는 전혀 평가되지 않을 수도 있습니다.
그리고 여러분이 생각해낼 수 있는 다른 많은 전략들이 있을 수 있습니다.

참고로 OCaml 언어 명세(language definition)에 따르면, (단락 연산자가 아닌 경우) 어느 쪽 피연산자를 먼저 평가할지는 명시되어 있지 않다(unspecified)고 합니다. 현재 OCaml 구현체(implementation)는 우연히 오른쪽 피연산자를 먼저 평가하지만, 프로그래머는 이에 의존해서는 안 됩니다.

많은 사람들이 왼쪽에서 오른쪽으로(left-to-right) 평가하는 것을 기대하므로, 우리는 --> 관계를 이에 맞게 정의하겠습니다.

먼저 왼쪽 피연산자가 단계를 진행할 수 있다는 규칙부터 시작합니다:

    e1 --> e1'
------------------- (BOP-L)
e1 bop e2 --> e1' bop e2

(규칙 BOP-L): 만약 왼쪽 피연산자 e1이 e1'으로 한 단계 진행한다면, 전체 표현식 e1 bop e2는 e1' bop e2로 한 단계 진행합니다.

만약 왼쪽 피연산자의 평가가 끝나 값(v1)이 되었다면, 오른쪽 피연산자(e2)가 단계를 진행할 수 있습니다:

    e2 --> e2'
------------------- (BOP-R)
v1 bop e2 --> v1 bop e2'

(규칙 BOP-R): 만약 왼쪽 피연산자가 값 v1이고 오른쪽 피연산자 e2가 e2'로 한 단계 진행한다면, 전체 표현식 v1 bop e2는 v1 bop e2'로 한 단계 진행합니다.

마지막으로, 양쪽 피연산자가 모두 값(v1, v2)에 도달했을 때, 이항 연산자가 적용될 수 있습니다:

v is the result of primitive operation v1 bop v2
--------------------------------------------------- (BOP-DO)
           v1 bop v2 --> v

(규칙 BOP-DO): 만약 v가 원시 연산(primitive operation) v1 bop v2의 결과라면, v1 bop v2는 v로 한 단계 진행(축약)합니다.

여기서 원시 연산(primitive operation)이란, bop 구문(+, *, <= 등)이 실제로 무엇을 의미하는지에 대한 기본적인 개념(underlying notion)이 있다는 것을 의미합니다. 예를 들어, + 문자는 단지 구문의 일부이지만, 우리는 그것의 의미를 산술 덧셈 연산으로 이해하도록 학습되었습니다. 원시 연산은 일반적으로 하드웨어(예: ADD 연산 부호)나 런타임 라이브러리(예: pow 함수)에 의해 구현됩니다.

이 과제에서 우리는 모든 원시 연산을 OCaml을 통해서 구현합니다. 즉, + 연산자는 OCaml의 + 연산자와 동일하며, *와 <=도 마찬가지입니다.

if 표현식 (If Expressions)

이항 연산자와 마찬가지로, if 표현식 (if e1 then e2 else e3)의 하위 표현식들(e1, e2, e3)을 평가하는 방식에도 여러 선택지가 있습니다. 그럼에도 불구하고, 대부분의 프로그래머는 조건문(guard) e1이 먼저 평가되고, 그 결과에 따라 두 분기(branches) 중 하나만 평가될 것으로 기대합니다. 대부분의 언어가 이런 방식으로 작동하기 때문입니다. 따라서 이러한 의미론(semantics)에 맞는 평가 규칙을 작성해 보겠습니다.

먼저, 조건문(e1)이 값으로 평가됩니다:

            e1 --> e1'
--------------------------------------- (IF-COND)
if e1 then e2 else e3 --> if e1' then e2 else e3

(규칙 IF-COND): 만약 조건문 e1이 e1'으로 한 단계 진행한다면, 전체 if 표현식은 if e1' then e2 else e3로 한 단계 진행합니다. 이 규칙은 조건문 e1이 값(이 경우 true 또는 false)이 될 때까지 반복적으로 적용됩니다.

그 다음, 평가된 조건문의 값에 따라, if 표현식은 선택된 분기 하나로 단순화(축약)됩니다:

-------------------------------------- (IF-TRUE)
if true then e2 else e3 --> e2

(규칙 IF-TRUE): 만약 조건문이 true로 평가되면, 전체 if 표현식은 then 분기인 e2로 한 단계 진행(축약)됩니다. else 분기인 e3은 평가되지 않습니다.

-------------------------------------- (IF-FALSE)
if false then e2 else e3 --> e3

(규칙 IF-FALSE): 만약 조건문이 false로 평가되면, 전체 if 표현식은 else 분기인 e3으로 한 단계 진행(축약)됩니다. then 분기인 e2는 평가되지 않습니다.

Let 표현식과 변수 (Let Expressions and Variables)

자 이제 let 표현식과 변수를 제외하고 모든 규칙을 서술했습니다. 하지만 let 표현식과 변수에 대한 규칙은 후술할 치환과 환경에 대한 개념이 필요하기에 후술하도록 하겠습니다.

hw3에 대한 다중 단계 평가 규칙 (Multi-step Relation)

이제 단일 단계 관계 -->를 정의했으므로, 다중 단계 관계 -->*를 정의하기 위해 특별히 더 할 일은 없습니다. 이는 단지 -->의 반사적 전이 폐쇄(reflexive transitive closure)일 뿐입니다. 다시 말해, 단지 다음 두 가지 규칙만으로 정의될 수 있습니다:

반사성 (Reflexivity): 어떤 표현식 e는 0 단계를 거쳐 자기 자신으로 다중 단계 진행합니다.
```
 --------- (MULTI-REFL)
 e -->* e
```
전이성 (Transitivity): 만약 e가 e'로 단일 단계 진행하고(e --> e'), e'가 e''로 다중 단계 진행한다면(e' -->* e''), e는 e''로 다중 단계 진행합니다 (e -->* e'').
```
   e --> e'     e' -->* e''
 -------------------------- (MULTI-TRANS)
            e -->* e''
```

물론, 인터프리터(interpreter)를 구현할 때는, 표현식이 값에 도달할 때까지 가능한 한 많은 단계를 진행하는 것이 실제로 우리가 원하는 것입니다. 즉, 우리는 오른쪽(-->*의 결과)이 단순한 표현식이 아니라 값(v)인 부분 관계(sub-relation) e -->* v 에 관심이 있습니다.

hw3에 대한 큰 단계 관계 평가 규칙 (Big-Step Relation)

큰 단계 관계(big-step relation) ==>를 정의하는 우리의 목표는 이것이 다중 단계 관계(multistep relation) -->*와 일치하도록 하는 것임을 기억하십시오 (즉, e ==> v 와 e -->* v 가 동치여야 합니다).

상수 (Constants) 는 간단합니다. 자기 자신으로 큰 단계 진행(big-step)하기 때문입니다:

--------- (BIG-INT)
i ==> i

---------- (BIG-BOOL)
b ==> b

(규칙 BIG-INT, BIG-BOOL): 정수 상수 i는 i로, 불리언 상수 b는 b로 큰 단계 진행합니다.

이항 연산자 (Binary Operators) 는 두 하위 표현식을 각각 큰 단계 진행시키고, 그 결과 값들에 원시 연산(primitive operation)을 적용합니다:

e1 ==> v1     e2 ==> v2     v is the result of primitive operation v1 bop v2
-------------------------------------------------------------------------- (BIG-BOP)
                                  e1 bop e2 ==> v

(규칙 BIG-BOP): 만약 e1이 v1으로, e2가 v2로 각각 큰 단계 진행하고, v가 원시 연산 v1 bop v2의 결과라면, e1 bop e2는 v로 큰 단계 진행합니다.

If 표현식 은 조건문(guard)을 큰 단계 진행시키고, 그 결과(반드시 true 또는 false)에 따라 해당 분기(branch) 중 하나를 큰 단계 진행시킵니다:

   e1 ==> true     e2 ==> v2
---------------------------------- (BIG-IF-TRUE)
if e1 then e2 else e3 ==> v2

(규칙 BIG-IF-TRUE): 만약 조건문 e1이 true로 큰 단계 진행하고, then 분기 e2가 v2로 큰 단계 진행한다면, 전체 if 표현식은 v2로 큰 단계 진행합니다.

   e1 ==> false     e3 ==> v3
---------------------------------- (BIG-IF-FALSE)
if e1 then e2 else e3 ==> v3

(규칙 BIG-IF-FALSE): 만약 조건문 e1이 false로 큰 단계 진행하고, else 분기 e3가 v3로 큰 단계 진행한다면, 전체 if 표현식은 v3로 큰 단계 진행합니다.

Let 표현식과 변수 (Let Expression and Variables): 작은 단계 평가 규칙과 마찬가지로 let 표현식과 변수에 대한 규칙은 후술하도록 하겠습니다.

치환 모델 vs. 환경 모델 (Substitution vs. Environment Models)

우리가 내려야 할 또 다른 선택지가 있는데, 이는 작은 단계(small-step)와 큰 단계(big-step)의 선택과는 직교(orthogonal)적인, 즉 독립적인 문제입니다.

변수(variable)의 구현에 대해 생각할 수 있는 두 가지 다른 방식이 있습니다:

첫째, 변수의 바인딩(binding)을 발견하는 즉시, 해당 이름의 유효 범위(scope) 전체에 걸쳐 변수 이름을 그 값으로 적극적으로 치환(substitute)할 수 있습니다.
둘째, 치환할 내용을 환경(environment)에 기록해두고, 변수 이름이 범위 내에서 언급될 때마다 이 환경에서 변수의 값을 조회(look up)할 수 있습니다.

이러한 아이디어는 각각 치환 모델(substitution model) 평가 방식과 환경 모델(environment model) 평가 방식으로 이어집니다.

작은 단계 vs. 큰 단계의 경우와 마찬가지로, 치환 모델은 수학적으로 다루기 더 좋은 경향이 있고, 환경 모델은 인터프리터(interpreter)가 실제로 구현되는 방식과 더 유사한 경향이 있습니다.

우리는 앞으로 큰 단계 평가 규칙과 환경 모델을 사용하여 인터프리터를 구현하도록 하겠습니다.

환경 모델 (Environment Models)

프로그램이 변수를 포함하게 되면 그 의미를 프로그래만 가지고 정의할 수 없고 변수의 현재 값을 알려주는 환경이 필요합니다. 예를 들어, 식 x + y의 의미는 변수 x와 y가 현재 어떤 값을 가지는지에 따라 달라집니다. 만약 x의 값이 1이고 y의 값이 2인 환경 {x: 1, y: 2}에서 계산하면 x + y의 값은 3이지만, {x: 2, y: 3}에서 계산하면 x + y의 값은 5를 가집니다.

앞으로 환경에 대해 다음의 표기법을 사용하겠습니다.

환경 p는 변수와 값을 매핑해주는 함수입니다.
{x: 1, y: 2} 는 변수 x와 y가 각각 1과 2로 매핑되어 있는 환경입니다. 그 밖의 다른 변수들에 대해서는 값이 정의되어 있지 않습니다.
환경 p에서 이름 x가 의미하는 값은 p(x)로 표기합니다. 위의 예에서 p(x)는 1입니다.
$\empty$는 빈 환경을 뜻합니다. 즉, 아무 변수도 정의되어 있지 않은 환경입니다.
{x: v}p는 주어진 환경 p에서 변수 x가 값 v를 의미하도록 확장한 환경을 의미합니다.

환경 모델에서의 큰 단계 평가 규칙

이제 평가 규칙에 환경이 포함되게 됩니다. 앞서 정의한 규칙들을 환경을 포함하는 삼항 규칙들로 바꾸도록 하겠습니다.

--------- (BIG-INT)
p ⊢ i ==> i

---------- (BIG-BOOL)
p ⊢ b ==> b

p ⊢ e1 ==> v1     p ⊢ e2 ==> v2     v is the result of primitive operation v1 bop v2
-------------------------------------------------------------------------- (BIG-BOP)
                                  p ⊢ e1 bop e2 ==> v

   p ⊢ e1 ==> true     p ⊢ e2 ==> v2
---------------------------------- (BIG-IF-TRUE)
p ⊢ if e1 then e2 else e3 ==> v2

   p ⊢ e1 ==> false     p ⊢ e3 ==> v3
---------------------------------- (BIG-IF-FALSE)
p ⊢ if e1 then e2 else e3 ==> v3

Let 표현식은 바인딩 표현식(e1)을 큰 단계 진행시키고, x와 바인딩 표현식의 값을 매핑한 환경에서 다시 e2 표현식을 큰 단계 진행합니다.

   p ⊢ e1 ==> v1     {x: v1}p ⊢ e2 ==> v2
------------------------------------ (BIG-LET)
       p ⊢ let x = e1 in e2 ==> v2

마지막으로, 변수 (Variables)는 큰 단계 진행 규칙을 갖지 않습니다. 이는 타입 정합적인(well-typed) 프로그램은 변수 이름 자체를 평가하려는 지점에 결코 도달하지 않을 것이기 때문입니다.

x =/=>

(여기서 =/=>는 “큰 단계 진행하지 않음”을 나타내는 표기입니다.)

과제 (hw4)

interpreter.ml을 수정하여 if expression과 let expression을 구현해주세요.

주의: interpreter.ml을 제외하고는 수정하실 수 없습니다.

환경 구현

type var = string
type value = Int of int | Bool of bool

type env = (var * value) list
let empty_env = []
let extend_env (x, v) e = (x, v) :: e

let rec apply_env x = function
    | [] -> failwith (x ^ " is not found")
    | (y, v) :: tl -> if x = y then v else apply_env x tl

큰 단계 평가 규칙 구현

let rec eval env = function
  | Var x -> apply_env x env
  | Int i -> Int i
  | Bool b -> Bool b
  | Binop (bop, e1, e2) -> begin
      match bop, eval env e1, eval env e2 with
        | Add, Int a, Int b -> Int (a + b)
        | Sub, Int a, Int b -> Int (a - b)
        | Mult, Int a, Int b -> Int (a * b)
        | Div, Int a, Int b -> Int (a / b)
        | Leq, Int a, Int b -> Bool (a <= b)
        | _ -> failwith "Operator and operand type mismatch"
      end
  | If (e1, e2, e3) -> begin
      (* 코드를 작성해주세요. *)
    end
  | Let (x, e1, e2) -> (* 코드를 작성해주세요 *)

실행 함수

let interpret s =
  let lexbuf = Lexing.from_string s in
    let ast = Parser.prog Lexer.read lexbuf in
      let value = eval empty_env ast in
        value