Program Analysis (??)

공부 문서 :
https://www.doc.ic.ac.uk/~herbert/teaching/PA4S.pdf

https://homepages.dcc.ufmg.br/~fernando/classes/dcc888/ementa/slides/ConstraintBasedAnalyses.pdf

http://staff.ustc.edu.cn/~yiyun/chapter/ConstraintBasedAnalysis.pdf

 

Principles of program analysis - Abstract 0-CFA Analysis

 

λ = 람다식

N ∈ Term λ-terms
x ∈ Var variables

 

N은 λ 의 일부 = N은 λ 식

x는 변수의 일부 = x 는 변수

 

N ::= x | (λx.N) | (N1N2)

 

람다식의 term 들에 대한 선언

x 변수  | 람다식 x의 바디 N | (N1N2) 함수호출 N1 함수를  N2 인자로 호출

 

 

Substitution:  (λx.M)N −→β M[x/N]

치환 : 람다식 x의 바디 M을 인자 N으로 실행. 

β M[x/N]

β : 베타리듀스

M : 위에서 적은 바디 M

[x/N] : x를 N으로 / (=치환)

문장으로 하면 : "람다식 x는 M을 본체로 갖고 N을 인자로 호출한다. 이를 베타리듀스 하면 본체 M의 x를 N으로 치환" 이 된다.

 

예를 들면, 람다식 x를 2로 호출하는 것을 베타리듀스하면,

 

람다식x 가 (x + 1)을 M으로 갖을 때 2를 인자로 호출하는 것은 곧,

x를 2로 치환하여 (2 + 1) 과 같다.

 

 

다음의 람다식이 존재할 때

(λx.x)z −→β z

(λx.x)(λy.y) 를 베타 리듀스하면 (λy.y) 가 된다.

 

 

 

e ∈ Exp  

e는 Expression의 부분, 즉 e 는 Expression = 라벨된 term

 

t ∈ Term

t 는 Term의 부분, 즉 t 는 term = 라벨되지 않은 Expression

 

e ::= tl

e (expression) 은 l (labelled) t (term) 이다.

 

t ::= c | x | fn x => e0 | e1 e2
| if e0 then e1 else e2 | e1 op e2
| let x = e1 in e2

 

• c: c는 상수(constant)를 나타냅니다. 예를 들어, 정수, 실수, 문자열 등의 상수가 될 수 있습니다.
• x: x는 변수(variable)를 나타냅니다. 변수는 값을 저장하거나 표현식에서 사용할 수 있는 이름입니다.
• fn x => e0: fn은 함수(function)을 나타내며, x는 함수의 매개변수(parameter) 이름이고 e0는 함수의 본체(body)입니다. 이 표현식은 함수를 정의하는 것을 나타냅니다.
• e1 e2: e1과 e2는 함수 호출(function application)을 나타냅니다. e1은 호출할 함수이고 e2는 함수에 전달할 인수(arguments)입니다.
• if e0 then e1 else e2: if-then-else는 조건문(conditional)을 나타냅니다. e0은 조건식(condition)이고, e1은 조건이 참일 때 실행되는 표현식이고, e2는 조건이 거짓일 때 실행되는 표현식입니다.
• e1 op e2: e1 op e2는 이항 연산자(binary operator)를 나타냅니다. 여기서 op는 연산자를 나타내고, e1과 e2는 연산자에 적용되는 피연산자(operands)입니다.
• let x = e1 in e2: let은 변수를 정의하고 사용하는 블록을 나타냅니다. x는 새로운 변수의 이름이고, e1은 변수에 할당될 초기 값이고, e2는 변수가 사용될 표현식이나 블록입니다.

 

예제:

((fn x => x1 )2 (fn y => y3 )4 )

제대로 복붙이 안되서 그런데 위 식에서 숫자는 label 입니다 (-_-; ) 이것때메 ChatGPT한테 물어보지도 못하네요 ㄷㄷ!

 

위 식은 세 절로 이루어져 있습니다. 바깥 절에서 보면 다음과 같은 구조입니다.

( (A)2 (B)4 )5

위 term 의 정의에서 e1 e2 의 형식입니다. 즉 함수 A 호출을 인자 B로 하는 expression 5 라는 뜻이 됩니다.

 

B 부터 해석하면 (fn y => y3 )4  이 식은 함수 선언이죠.

이 함수는 y를 매개변수로 갖는 y3 라는 expression 을 갖는 함수이고 ()4 는 expression이라는 뜻이죠

 

A 는 마찬가지로  (fn x => x1 )2 은 이 함수()2 는 x를 매개변수로 갖고 x1 를 바디로 갖는다는 뜻입니다.

 

 

다른 예제를 한번 풀어보죠.

 

let f = fn x => x 1;
g = fn y => y + 2;
h = fn z => z + 3

in (f g) + (f h)

 

위 식은 다음처럼 풀립니다.

(f g) + (f h) −→ ((fn x => x 1) g) + ((fn x => x 1) h)
−→ (g 1) + (h 1)
−→ ((fn y => y + 2) 1) + (fn z => z + 3) 1)
−→ (1 + 2) + (1 + 3)
−→ 7