[노윤철]

안녕하세요?
숙제 7 중 올바르게 작동하기는 하지만 타입을 알 수 없는 경우가 있는 것 같아 질문 드립니다.

[안중원]

안녕하세요, 프로그래밍 언어 조교 안중원입니다.

우선 숙제에 관해서는, 제시하신 프로그램과 같이 전체 식의 타입이 한가지로 결정되지 않는 경우에 관해서는 채점하지 않을 예정입니다. 숙제 코드를 작성하실 때에는 입력 프로그램이 한 가지 타입으로 결정되거나 올바른 타입이 없는 경우만 가정하셔도 좋습니다.

그 외에 궁금해하실 만한 점에 대해서도 답변드리겠습니다.

제시하신 프로그램은 단순 타입 시스템에서는 i, b, s 가운데에서 어떤 타입이든 될 수 있다고 말해도 좋습니다. 맥락에 따라 다를 수는 있으나, 일반적으로 타입 시스템 상으로 올바르다는 말은 "그 프로그램에 대해서 타입 규칙을 따르는 증명 나무를 만들 수 있다"라는 뜻으로 이해하시면 됩니다. 제시하신 프로그램에 관해서는 그러한 증명 나무를 만드는 방법이 3가지가 있는 것이니, "타입 시스템 상에서 틀렸다"라고 말할 수는 없는 셈입니다.

이러한 해석은 타입 안전성(soundness) 정의에 비추어보아도 자연스럽습니다. 프로그램에 대해 올바른 타입이 하나 이상 있다면, 그 프로그램의 실행 중에는 타입 오류가 일어나지 않습니다. 이는 올바른 타입의 개수가 하나냐 셋이냐 하는 점과는 무관하게 얻을 수 있는 확증입니다.

질문 자체와는 약간 별개이지만 한가지 정정을 드리자면, M 언어의 실행의미는 큰걸음(big-step) 방식으로 정의되므로 무한루프는 정상적인 실행의 범주에 속하지 않습니다. 일반적으로 큰걸음 방식에서는 (타입 시스템에서와 비슷하게) "실행 규칙을 따르는 유한한 증명 나무를 만들 때 우변에 나올 수 있는 값들"로 프로그램의 실행의미를 정의합니다. (가끔 무한한 증명 나무를 다루기도 하지만 일반적인 경우는 아닙니다.) 제시하신 프로그램으로는 실행 규칙을 따르는 유한한 증명나무를 만들 수 없기 때문에 어떠한 실행의미를 가진다고 말하기 어렵습니다.

이렇듯 큰걸음 의미구조에서는 무한한 실행을 다루기 까다로워 타입 안전성을 논할 때에는 작은걸음(small-step) 방식이 일반적으로 선호됩니다. 수업에서 다루는 타입 안전성 증명, 통칭 progress & preservation lemma를 통한 증명에서도 작은걸음 의미에 대하여 증명하는 것이라고 보시면 됩니다.

감사합니다.
_________________
TA 안중원
e-mail: jwahn@ropas.snu.ac.kr