[연재] 프로그래밍 언어의 의미를 정의하는 법

[다믜(damhiya)]

https://github.com/damhiya/Presentations/blob/master/PL%20and%20Logic/main.pdf

명령형 프로그래밍 언어의 의미를 정의하는 방법에 대해 소개하는 자료를 만들어 봄

발표에서 말로 설명하면 PL전공 아닌 사람도 이해시킬 수 있을것 같은데 슬라이드만 보고 이해가 갈지는 잘 모르겠다

[익명(buypostal4)]

잘썼네 그냥 궁금해서 물어보는건데 trace기반 정의가 deterministic program의 경우에는 투머치인거 아님? formal verification만 놓고 봤을 때 따로 장점이 있음? 트레이스 분류 만들어봤자 어디 들어가는지 체크하는 것도 쉽지 않을 것 같은데...

[다믜(damhiya)]

저게 사실 뒤에 프로그램의 스펙을 어떻게 줄 수 있는지, 증명은 어떻게 하는지 이런 내용도 다룰려다가 분량 때문에 프로그램의 의미 까지만 다룬건데. 스펙을 다루는 방법중에는 호어로직, 전이 시스템, 트레이스 세가지가 있음. 호어로직은 상태와 관련이 있고, 전이 시스템은 상태와 이벤트에 관련이 있고, 트레이스는 이벤트에만 관련이 있음

[다믜(damhiya)]

그래서 프로그램의 성질을 이벤트에 집중해서 서술하고 싶은 경우에는 호어로직 보다는 전이 시스템이랑 트레이스가 유리함. 이건 프로그램이 결정적이더라도 그렇지.

[다믜(damhiya)]

그리고 전이 시스템이랑 트레이스를 비교하자면, 트레이스가 좀 더 외연적인(extensional) 정의라는 점에서 차이가 있음. 트레이스의 정의는 상태와 무관하니까 내부 구조는 무시하고 외부에서 구분되는 성질에 집중한다는거지.

[익명(buypostal4)]

그럼 semantics 정의 주는 방식에 따라서 같은 semantics인 프로그램도 서로 달라지지 않나? 이건 검증에서는 별 상관 없으려나

[다믜(damhiya)]

이런 외연적인 특성 때문에 트레이스를 다루는게 더 편리한 상황이 있음

[다믜(damhiya)]

그렇지. 예를 들어 Big-step semantics에서는 종료 안하는 프로그램들을 서로 구분할 방법이 없는데, Small-step semantics나 트레이스에서는 diverge인지 reactive diverge인지 구분할 수 있게된다던가. 오히려 세밀하게 구분이 가능한건 좋은거임

[다믜(damhiya)]

그리고 "어느 트레이스 분류에 들어가는지 체크하는게 어렵다" 이건 트레이스 분류가 트레이스를 정의할 때 조심해야 하는 부분이라 소개한거고, 프로그램 검증에선 어차피 프로그램을 거의 100% 완전히 파악해야 가능한거라 별 상관 없음.

[다믜(damhiya)]

예를 들어 reactively diverge 하는 프로그램하고 termination하는 프로그램은 증명에 대한 접근부터 달라질 가능성이 큼

[익명(buypostal4)]

그렇구나 애초부터 뭐가 어떻게 돌아가는지는 파악을 해야 시작을 한다는거네. collatz function 같은 거 생각하고 있었음

[익명(58.237)]

이건 그냥 갤에 보여주는거고 학회같은데선 위키피디아 인용 안 하지?

[다믜(damhiya)]

당연 ㅋㅋ 학회는 아닌데 교수님이 저 문장을 인용하셨길래 넣었음

[black7375(221.168)]

이와중에 tex로 만들어진 문서네