Question #1: What is the value of the following expression? ➡ (2 + 3)
expr + expr 형태이므로 syntatically valid한 expression이다.
evaluation result는 5이다.
Question #2: What is the value of the following expression? ➡ (fun x y -> 5) 7
syntatically valid한 expression이다. 함수 정의를 정의하고 호출하는 문법이다.
evaluation result는 ? 알 수 없다.
이 함수는 2개의 parameter를 받는데, 현재 7 하나만 전달하고 있다.
➡ 이 expression은 syntatically valid하지만, semantically 문제가 있는 Ill-formed expression이다. 우리는 이러한 ill-forme expression은 evaluate하지 않을 것이다!
Question #3: What is the value of the following expression? ➡ (fun x -> 5) + 7
syntatically valid한 expression이다.
evaluation result는 ? 알 수 없다.
fun x -> 5는 함수이다. 즉 함수 + 정수인데, 이것은 Numeric Operation은 수를 기대했지만 함수가 덧셈의 대상이 되었다.
➡ 이 expression은 syntatically valid하지만, semantically 문제가 있는 Ill-formed expression이다. 우리는 이러한 function expression은 + form 안에 들어갈 수 없도록 정할 것이다!
Question #4: What is the value of the following expression? ➡ ((fun x -> x) 5) + 7
syntatically valid한 expression이다.
➡ fun x -> x는 function expression인데, + form에 들어왔으므로 우리가 만든 룰에 따라 ill form이다.
evaluation result는 ?
(fun x -> x)은 function이지만, 5가 application되고 있으므로 (fun x -> x) 5는 5가된다. 따라서 12가 결과가 된다.
➡ 이 케이스를 well form 이 되도록 rule을 바꿔보자.
function expression는 + form 안에 immediately inside 이지 않은 경우는 가능하다.
Question #5: What is the value of the following expression? ➡ ((fun x -> x) (fun y -> y)) + 7
syntatically valid한 expression이다.
➡ 이 케이스는 우리의 룰에 따라 well form expression이다. + form에 function expression에 immediately inside이지 않기 때문이다.
➡ evaluation result는 ? 없다.
함수 둘 다 모두 identity function이며, application 한다고 해도 무한 반복된다.
➡ 룰을 바꿔서 해당 케이스가 ill form으로 만들어보자.
Question #6: Is it possible to define well-formed (as a decidable property) so that we reject all expressions that produce errors?
오류를 생성하는 식만 거부하도록 잘 구성된(결정 가능한 속성으로) 정의하는 것이 가능할까?!
그렇다. 모든 expression을 reject한다면.
➡ but 모든 expression을 reject하는 바는 우리가 원하는 것이 아니다 ..
Question #7: Is it possible to define well-formed (as a decidable property) so that we reject only expressions that produce errors?
오류를 생성하는 식만 거부하도록 잘 구성된(결정 가능한 속성으로) 정의하는 것이 가능할까?!
아니다.
🔔 Halting Problem
"주어진 프로그램이 해결하고자 하는 문제가 해결 가능한지 말해줄 수 있는 일반화된 알고리즘이 존재하는가?" 라는 질문 => 일반화된 방법은 없다라는 결론.
general solution이 없다는 문제이다.
x++y는 FVAE 언어에 따르면 incorrect syntax이다.
-> 해당 영역은 syntatically invalid 영역이다.(fun x->5) + 7은 FVAE 언어에 따르면 Valid syntax이다. 그러나, semantically incorrect하다.
-> 해당 영역은 syntatically correct & semantically incorrect 한 영역이다.5+5는 semantic, syntatically 모두 correct하다.
-> 해당 영역은 syntatically correct & semantically correct 한 영역이다.
=> 우리는 오직 가장 안쪽, 모두 correct한 마름보 영역의 프로그램만을 accept하기를 원한다.
그러나 이것은 우리의 halting problem이다.
(1) 전체 valid program 중에서도, 오직 some type of the program만을 accept하게 한다. (some valid program 을 reject하게 한다)
- 장점 : runtime error가 존재하지 않는다
- 단점 : 옳은 program도 reject될 수 있다.
(2) 모든 valid program을 accept하지만, some invalid program도 일부 accept한다.
- 장점 : 옳은 program은 모두 accpet도니다.
- 단점 : runtime error가 존재
=> expression에 type을 줌으로써, 해당 expression이 well form, ill form인지 파악할 수 있다.
🌳 Type
expression에 type을 부여함으로써, Dynamic Analysis, Static Analysis를 통해 해당 expression이 well form인지 아닌지 파악할 수 있다.
이를 찾기 위해 동적분석과 정적분석, 2가지 방법이 있다.
📌 Dynamic Analysis
실제 프로그램을 run하여 테스트한다.
모든 possible case를 잡아내지 못한다. 예를 들어 num이 integer일 경우 integer값을 실제로 넣어보면서 테스트해야 하는데, 모든 범위를 넣을수 없으므로 한계가 있다.
만약 error가 나온다면 실제로 정말 error인 것이다.
📌 Static Analysis
프로그램을 실제로 execute하지 않고, 코드를 보고syntatically 체크한다.
모든 possible combination의 cases를 검사할 필요가 없고, expression을 검사함으로서 wellform인지 아닌지 파악할수 있다. 따라서 모든 possible case를 파악할 수 있다.
그러나 over approximate하기 때문에 실제 런타임 에러가 아닌데 런타임 에러라고 잘못 파악할 수 있다.
-> 우리는 execute하지 않고 분석할 것이다.
🌱 type 은 value의 집합이다.
예를 들어, integer type은 1, 2, 3, 0, -1등 정수 value들의 집합이다.
🌱 type error
unexpected type이 나타난 경우 타입 에러이다.
(fun x->5) +7에서 함수라는 타입을 expect하지 않고 int를 expect했기 때문에, type error이다.
(ʎx.x)+1 역시 함수+num 타입인데, num 타입이 와야 하는데 기대하지 않은 함수 타입이 왔으므로 type error이다.
🌳 Type Check and Interpret
Evaluate를 위해서는, typeCheck을 먼저 수행한 후 interpret를 한다.
🌱 typeCheck
typeCheck(e) = t
Γ⊢ e : tΓ 는 type 정보를 저장하는 enviroment이다.
enviroment Γ 에서, expression은 type t를 가리킨다.
🌱 Interpret
interp(e) = v// value v를 return한다는 뜻 (ocaml)
σ⊢ e ⇓E v// environment σ에서 expression e를 v로 evaluate한다.
