🌱 NAE를 VAE로 확장하기
NAE에 변수를 추가함으로써, 언어 VAE("Variable and NAE")로 확장해 보자.
✔ NAE에 변수를 추가한다. 변수의 이름은 Identifier이다.
✔ 모든 변수는 immutable하다고 가정한다. (ocaml 처럼!)
즉, 한번 변수가 값에 bound된다면 그 변수는 udpate될 수 없다.
1) syntax 추가
변수 정의 추가
let var = expr in expr : variable binding scope
변수 접근 추가
var
2) Abstract Syntax 나타내기
기존에는 정수 집합 Z뿐이었는데, Var이 추가된다.
Tree의 형태로 나타내면, id노드와 lETin 노드를 만들 수 있다.
3) Semantics of VAE
이와 같이 abstract memory를 이용하여 VAE의 semantic을 정의할 수 있다.
📌 rule LetIn
LetIn 문법으로 변수를 정의하도록 VAE 문법을 확장했는데,
이에 대한 semantic은 다음과 같다.
abstrac memory σ 에서, e1이 n1으로 계산된다면 x의 값을 n1으로 update해주는데, 그 상태에서 e2가 n2로 계산된다면 전체 expression(let x = e1 in e2)의 결과는 n2가 된다.📌 rule Id
x가 abstrac memory σ에 있다면, x는 σ(x)가 된다. 즉 abstract memory에서 x의 값을 가져온 값이다.
📌 x가 σ에 있을 때, σ ⊢ x 는 σ(x)로 평가된다.
📌 x가 σ에 정의되지 않았을 때, σ ⊢ x 는 error로 평가된다.
📌 e1이 n1으로 평가된다. 그렇다면 abstract memory를 업데이트한 σ[x↦n1] 이 상태에서 e2가 n2로 평가된다면
let x = e1 in e2는 n2로 평가된다.
5) Proof of VAE
let x = 1 in x + 3이 4로 평가된다는 것을 증명해보자.
let x = 3 in x + x이 6로 평가된다는 것을 증명해보자.
let x = 3 in let x = x + 1 in x - 3이 1로 평가된다는 것을 증명해보자.
