- 제출방법 : 작성한 프로젝트를 ‘{학번}’라는 이름으로 저장한 후 압축하여 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