Functions and VAE, 즉 'F1VAE'로 확장해 보자!
즉 VAE에 First Order Function을 더해보자.
아래와 같은 syntax들이 가능하도록 function을 추가할 것이다.
1. 함수
함수란 특별한 action을 수행하는 코드 조각이다.
터미널에 string을 출력하는 printf, input을 받고 string으로 변환하는 read_line 도 모두 함수이다.
1) High-order function
인자로서 함수를 받고, 함수를 리턴할 수 있는 함수를 high-order function이라고 한다.
high-order function이 가능한 언어를 함수와 변수를 똑같이 취급한다.2) First order function
First order function은 함수를 인자로 받거나 리턴하지 않는 함수로서,
함수를 변수와 다르게 취급한다.
함수를 변수처럼 인자로 함수에 넘겨주거나, 리턴할 수 없다.
c나 자바 등 대부분의 Imperative 언어(non-functional 언어)는 first order function을 지원한다.
-> F1VAE는 First Order Function을 지원한다고 가정해 보자!
VAE에서는 abstract memory 하나였는데, F1VAE 변수와 함수를 다르게 취급하기 위해 memory가 두개 필요하다.
2. F1VAE로 확장하기
1) Concrete Syntax of F1VAE
prog ::= decl expr
F1VAE는 하나의 함수 정의와 하나의 Expression으로 이뤄진 프로그램이다.
number, var: VAE와 동일하다.
prog: F1VAE 프로그램을 의미한다.
decl: 인자를 받는 함수의 정의를 의미한다.
var(expr): 함수 호출을 의미한다.
2) Abstract Syntax of F1VAE
위와 같이 prog 노드, Fundef 노드, call노드를 추가할 수 있다.
abstract syntax에서는 concrete의 불필요한 디테일을 삭제하므로, concrete에서의 endef는 삭제된다.
📌 현재 F1VAE는 오직 하나의 파라미터만을 가질 수 있다 ❗❗
현재 def var var로 정의했기 때문에, multiple 파라미터는 허용되지 않는 상태이다.
Abstract Syntax of F1VAE : in OCaml
3) Abstract Memory of Functions
🌱 함수 정의를 저장하기 위한 Abstract Memory를 정의해야 한다.
Fstore: 함수 이름을 받고, 파라미터와 함수 바디 (x,e)를 쌍으로 리턴하는 함수들의 집합
Fstore : Var->Var x E
Λ는Fstore의 요소이다.
Λ∈Fstore
🌱 Abstract Memory를 이용하기 위해 두개의 helper 함수를 정의하자.
1)
Λ(x): 추상 메모리 Λ로부터, x를 찾고 그 값을 리턴한다. (getter 함수)
즉 주어진 함수의 이름 x에 대한 매개변수와 함수 바디의 쌍을 찾는다.
2)Λ[x1 ↦ (x2, e)]: 추상메모리 Λ를 업데이트하는 함수이다.
x1는 함수 이름, x2는 매개변수 이름, e는 함수 본문을 의미한다. 이 함수는 추상메모리 Λ의 값을 변경하여 x1을 x2와 e의 쌍으로 맵핑하여 파라미터와 바디를 업데이트하고, 새로운 추상메모리 Λ를 리턴한다. (setter 함수)
Ocaml로 다음과 같이 Abstract Memory for Functions를 구현할 수 있다.
이 표현은 추상 메모리를 업데이트하고 조회하는 방식을 나타낸다.
x1과 x'가 동일한 경우: x1은 함수의 이름이며, x'은 현재 조회하려는 함수의 이름이다. 이 경우, 업데이트된 추상 메모리는 (x2, e)로 변경된다. 여기서 x2는 함수의 매개변수이고, e는 함수의 본문이다. 따라서 업데이트된 추상 메모리에서 x'를 조회하면 (x2, e)를 반환한다.
x1과 x'가 다른 경우: x1은 업데이트할 함수의 이름이며, x'은 현재 조회하려는 함수의 이름이다. 이 경우, 추상 메모리는 변경되지 않고 그대로 유지된다. 따라서 업데이트된 추상 메모리에서 x'를 조회하면 여전히 이전의 값인 Λ(x')를 반환한다.
4) Semantics of F1VAE
✔ Semantics에서 기존에는 σ 뿐이었지만, "Λ"가 추가되었다.
ex) rule ADD
Λ & σ 하에서, e1의 계산 결과가 n1이고, e2의 계산결과가 n2라면 e1 + e2는 n1 +z n2로 계산된다.
🔔 rule Prog
d e
[rule Prog] : 프로그램(p)이 함수 정의(d)와 식(e)로 구성된 경우를 처리하는 규칙.
1. 프로그램(p)은 함수 정의(d)와 식(e)로 구성
2. 함수 정의(d)는 추상 메모리 Λ에 대해 평가. 이때, 추상 메모리 상태는 비어있3. 는 상태(empty memory)
4. 함수 정의(d)가 평가되면, 추상 메모리 Λ에는 함수 정의 내용이 저장
5. 이후, 식(e)가 평가된다.
6. 만약 식(e)의 평가 결과가 정수 n이라면, 프로그램 p의 결과는 nex)
def add x y = x + y endef
add 3 4
1. 함수 정의(def)인 def add x y = x + y endef를 추상 메모리에 평가. 이때, 추상 메모리는 빈 상태(empty memory)
2. 함수 정의가 평가되어 추상 메모리에 add ↦ (x, y) = x + y가 저장
3. 그 다음, 식(expr)인 add 3 4를 평가
4. 함수 호출 add 3 4에서 add는 추상 메모리를 통해 함수 정의를 찾는다. 추상 메모리에 저장된 add ↦ (x, y) = x + y를 찾는다.
5. 함수 정의에서 x와 y를 각각 3과 4에 바인딩하여 x + y를 계산
6. 3 + 4는 7로 평가
7. 따라서 프로그램의 결과는 7
🔔 rule FDEF
def x1 x2 = e
def x1 x2 = e는[x1 ↦ (x2, e)로 계산된다.
그렇다면, rule FCall x(e)는 어떻게 정의할까?!
🌱 Approach (1). Substitution
"치환"을 사용하여 함수 호출을 처리한다. 파라미터 변수를 함수 바디에 전자된 인자값으로 대체하는 방식이다!
✅
e[n/x]: 표현식 e에서 x로 바운드 된(bound occurence) 변수를 n으로 대체하라.Example)
(x+1) [4/x] => x + 1
(let x = 1 in y+3) [1/y] => let x=1 in 1+3[rule FCall] : x(e)의 시맨틱 정의
Λ과 σ가 주어진 상황에서, e의 평가 결과가 n1이고, Λ(x)가 (x1, e1)인 경우에,
(= 함수 바디는 e1, 매개변수는 x1, 인자는 n1(e)일 때)
그리고 Λ과 빈 메모리 상태에서 e1[n1/x1]의 평가 결과가 n2인 경우,
x(e)는 n2가 된다.참고사항 : "Λ & ∅"는 추상 메모리(Λ)와 빈 메모리(empty memory)를 함께 나타내는 표기법이다. 이는 추상 메모리에 어떤 함수 정의나 매핑이 없음을 나타낸다.
🌱 Approach (2). Using Store
저장소 (Store)을 사용하여 함수 호출을 처리한다.
파라미터 변수와 전달된 인자 매핑을 추상 메모리에 추가한 후, 함수의 본문을 계산한다.[rule FCall] : x(e)의 시맨틱 정의
Λ과 σ가 주어진 상황에서, e의 평가 결과가 n1이고, Λ(x)가 (x1, e1)인 경우, 그리고 Λ과 [x1 -> n1]을 사용하여 e1의 평가 결과가 n2인 경우, x(e)는 n2가 된다.
🌱차이점
Subsitute 방법에선 abstract memory를 사용하지 않았으므로 공집합이지만 Using Store 방법에선 Abstract memory를 이용한다.
Approach 1: Substitution
함수 호출 시 함수 본문에서 매개 변수 변수를 호출 인자 값으로 치환(substitution)하는 방식을 사용한다. 즉, 함수 호출을 처리할 때, 함수 본문에 있는 매개 변수 변수를 호출 인자 값으로 대체하여 본문을 실행한다.
[rule FCall]에서 "Under Λ & ∅"를 사용하는 경우, σ는 빈 메모리(empty memory) 상태에서 함수 호출을 처리하며, 호출 인자 값을 함수 본문의 매개 변수 변수에 대입하여 실행한다.Approach 2: Using Store
함수 호출 시 추상 메모리에 매개 변수 변수와 인자 값을 매핑하여 함수 본문을 실행하는 방식을 사용한다. 즉, 함수 호출을 처리할 때, 추상 메모리에 매핑 정보를 추가하여 함수 본문을 실행한다.
[rule FCall]에서 "Under Λ & σ"를 사용하는 경우, σ는 함수 호출에 필요한 변수와 값의 매핑 정보를 포함하는 메모리 상태를 나타낸다. 함수 호출 시 해당 함수의 매개 변수와 인자 값을 매핑하여 추상 메모리에 저장하고, 그 상태에서 함수 본문을 실행한다.
5) Formal Semantics of F1VAE
Rule Prog
함수 정의 d가 Λ(lamda)로 평가될 경우, 메모리에 d가 저장되고 메모리는 업데이트 된다. Λ와 empty memory 하에서, (변수 메모리가 empty memory인 이유는 변수를 아직 정의하지 않았기 때문이다) 만약 e의 결과가 n이라면, d e는 n이다.
주의사항
⇓F : evaluate as function
⇓e : evaluate as expression
⇓p : evaluate as program evaluation
Rule FDef
def x1 x2는[x1 -> (x2, e)]로 evaluate된다.
[x1 -> (x2, e)]는 새로운 abstract memory를 의미한다
x1함수는 x2 파라미터와 e 함수 바디에 bound된다.
따라서 이def x1 x2는[x1 -> (x2, e)]정보를 가진 new abstract memory에 bound된다.
Rule Fcall : substitution approach
