덴마크편 · 연재 60PART I · 01–05
대출 장부와 식의 한 단계
도서관 화면에 ‘대출 승인’이 뜨기까지 무엇이 달라졌나요?
민서가 책 두 권을 빌린 뒤 세 번째 책을 올려놓습니다. 대출기는 대출 수를 하나 늘리고, 세 권 이하면 승인 화면으로 갑니다. 마지막 글자만 읽어서는 수를 언제 바꿨는지 모릅니다. 플롯킨은 지금 남은 프로그램과 지금 가진 자료를 하나의 구성으로 묶고, 한 구성에서 다른 구성으로 가는 화살표를 적습니다.
사회자 장부의 2가 먼저 3이 되나요, 아니면 세 번째 책을 받을 수 있다는 판정이 먼저 나오나요?
답변 대입이 끝난 뒤 조건을 읽어야 합니다. 처음의 2를 보고 승인했어도 이번 화면은 우연히 같았을 겁니다. 처음부터 세 권이었던 독자로 바꿔 보세요. 갱신한 4를 읽으면 거절하고, 옛 3을 읽으면 잘못 승인합니다.
원문·범위 · §§1.1–1.2, 3–5쪽. 대출기는 편집부 사례.
처음이 한 권이라면, 마지막 검사에서 읽는 수는 얼마일까요?
두 권입니다. 검사는 새 장부에서 2 ≤ 3을 읽습니다.
전이 화살표 하나에 어떤 약속이 들어 있나요?
구성의 집합 Γ와 그 위의 이항관계 →를 정합니다. γ → δ라고 쓰면 γ에서 δ로 바로 갈 수 있다는 뜻입니다. 정상 종료를 구분할 때에는 나가는 화살표가 없는 구성들 가운데 최종 집합 T도 따로 지정합니다. 화살표가 없다는 사실만으로 T에 넣을 수는 없습니다.
사회자 대출 수를 읽고 더하는 일을 화살표 하나로 묶어도 되나요?
답변 규칙을 어떻게 정했는지에 달려 있습니다. 이 글의 확대 모형에서 books+1은 장부를 읽어 2+1이 되고, 다음에 3이 됩니다. 원문의 명령 규칙은 우변을 끝까지 계산한 증거를 한 대입 화살표의 전제로 둡니다. 같은 작업을 보아도 세는 대상이 다릅니다.
원문·범위 · §1.2, 정의 1–2, 4–5쪽. §3.2 대입 규칙, 33쪽.
γ → δ이면 δ → γ도 따라오나요?
그렇지 않습니다. 역방향 이동을 허용하는 규칙이 따로 있어야 합니다.
프로그램이 같은데 왜 장부까지 구성에 넣을까요?
〈books+1, σ〉의 앞은 남은 식이고 뒤는 저장소입니다. σ(books)가 2인 독자와 8인 독자에게 같은 문자 books를 보여도 다음 식이 달라집니다. 이 예에서 식을 읽는 동안 σ는 보존되고, 대입이 일어나는 순간에만 저장소가 바뀝니다.
사회자 식이 3이 되는 순간에 대출 장부도 이미 3인가요?
답변 아직 2입니다. 종이 메모에 합계 3을 계산하는 일과, 대출기에 그 수를 기록하는 일은 다른 규칙입니다. 〈books := 3, 2〉에서 대입해야 〈skip, 3〉이 됩니다. 뒤 그림에서 숫자가 어느 쪽 칸에 있는지 확인해 보세요.
원문·범위 · §3.1.1, 28–29쪽, 변수 규칙. §3.2, 32–33쪽.
〈books+1, 8〉에서 변수 읽기 직후의 구성은?
〈8+1, 8〉입니다. 계산 결과 9는 아직 나오지 않았습니다.
큰 식의 한 단계를 어떻게 증명하나요?
가로선 위의 전제를 먼저 확인하고 아래 결론을 읽습니다. 1+2가 3으로 갈 수 있다면 큰 식 (1+2)+(3+4)도 3+(3+4)로 갈 수 있습니다. 위 전이와 아래 전이는 두 번 연이어 실행한 기록이 아닙니다. 위 전이가 아래의 단 한 번을 정당화합니다.
사회자 숫자를 보자마자 큰 식을 곧바로 10으로 바꿔도 되나요?
답변 큰 식의 바로 아래 두 피연산자는 아직 합식입니다. 두 수를 바로 더하는 기본 규칙의 전제가 성립하지 않습니다. 먼저 왼쪽 덧셈을 한 뒤, 3+7까지 와야 마지막 덧셈 규칙을 쓸 수 있습니다.
원문·범위 · §3.1, 25–27쪽, 덧셈 규칙 1–3.
어떤 조건에서 기본 덧셈을 쓸 수 있나요?
현재 덧셈 바로 아래의 양쪽이 모두 수일 때입니다.
어느 쪽부터 계산할지는 누가 정하나요?
왼쪽 우선 규칙은 먼저 왼쪽을 움직입니다. 왼쪽이 수가 되면 오른쪽의 전이를 올리고, 둘 다 수이면 합을 냅니다. 같은 식에 오른쪽 우선 규칙을 대신 넣으면 맨 처음 나오는 구성이 달라집니다. 실험 1에서는 순서만 바꿔 이 차이를 볼 수 있습니다.
사회자 결과가 모두 10이라면 이 순서는 관찰할 수 없는 차이인가요?
답변 최종 수만 기록하면 두 실행은 같은 칸에 들어갑니다. 첫 화살표를 기록하면 왼쪽 우선은 3+(3+4), 오른쪽 우선은 (1+2)+7입니다. 이 식에는 부작용도 오류도 없으므로 이 사례에서 최종값 차이까지 발견했다고 말할 근거는 없습니다.
원문·범위 · §3.1, 25–27쪽. 오른쪽 우선은 비교용 변형.
이미 3+7이라면 왼쪽부터와 오른쪽부터의 첫 결과는?
두 경우 모두 10입니다. 어느 쪽의 부분식도 더 움직일 수 없습니다.
PART II · 06–10
일곱 번의 전이와 유도의 근거
도서관 예제는 승인까지 모두 몇 단계인가요?
교육용 확대 모형에서 일곱 단계입니다. 대입 우변에서 ① books를 2로 읽고 ② 2+1을 3으로 계산합니다. ③ 장부에 3을 쓰고 ④ skip ; C에서 앞의 skip을 벗깁니다. 조건에서 ⑤ books를 3으로 읽고 ⑥ 3 ≤ 3을 true로 계산한 뒤 ⑦ 승인 가지 lend를 고릅니다. 여기서 C는 조건문 전체이고 lend와 deny는 최종 화면 표지입니다.
사회자 원문 33쪽을 보고 세었더니 수가 더 적습니다. 어떤 줄에서 달라졌을까요?
답변 플롯킨의 대입 규칙은 우변의 여러 식 단계를 전제로 묶어 한 번에 최종 저장소로 갑니다. 그 저장소를 순차명령이 이어받습니다. 조건 규칙도 참거짓을 얻기까지의 계산을 전제로 둡니다. 이 글은 읽기와 쓰기를 화면에서 분리하려고 skip과 조건 내부 전이를 따로 두었습니다. →*는 0번을 포함해 여러 번 이어 감을 표시합니다.
원문·범위 · §§3.2–3.3, 32–35쪽. 7단계와 skip·≤·화면 표지는 편집부 규칙.
처음부터 3권이어도 일곱 단계를 거치나요?
그렇습니다. ③에서 4가 되고 ⑥에서 4 ≤ 3이 거짓이므로 ⑦에서 deny를 고릅니다.
유도 나무와 실행 기록을 어떻게 구별하나요?
실행 기록은 방금 얻은 구성을 다음 화살표의 출발점으로 잇습니다. 유도 나무는 지금 주장하는 화살표 하나를 받치는 전제를 쌓습니다. 순차명령의 앞이 움직여 저장소 3을 만들었다면, 그것을 감싸는 결론에도 같은 3을 적어야 합니다.
사회자 규칙 이름만 맞추고 마지막에 저장소 2를 쓰면요?
답변 앞 명령 books := 3이 2를 받아 3을 남겼다는 전제를 사용해 놓고, 큰 명령에는 2를 적는다면 서로 맞지 않습니다. 실험 2에서 마지막 저장소만 2로 바꾸어 반례를 확인할 수 있습니다. 반대로 if true의 가지를 고르는 전제에서는 장부 2가 그대로입니다.
원문·범위 · §3.1, 26–27쪽, 유도 예시. §3.2, 33–34쪽, 순차명령 규칙.
순차명령의 전제가 저장소 3을 주었을 때 4를 적을 수 있나요?
그 규칙으로는 안 됩니다. 새 대입 없이 저장소가 한 번 더 바뀌었다는 잘못된 결론입니다.
‘구조적’이라는 말에서 무엇의 구조를 보나요?
현재 프로그램의 바깥 문법 모양을 봅니다. 맨 바깥이 덧셈이면 덧셈 규칙을 살피고, 순차명령이면 그 앞 명령의 전이와 앞이 이미 끝났을 때의 규칙을 살핍니다. 같은 숫자 3이 보인다고 책 수를 대입하는 규칙과 두 수를 더하는 규칙을 뒤섞지 않습니다.
사회자 skip ; C에서 C가 아주 복잡해도 첫 단계가 정해지나요?
답변 이 글의 순서 제거 규칙은 C를 그대로 남깁니다. C 안을 계산할 필요가 없습니다. 반대로 (if true then A else B) ; C는 앞이 아직 skip이 아니므로 조건문 전이를 확인한 뒤 순차명령에 올립니다. 두 경우의 차이는 바깥과 바로 아래의 모양에서 드러납니다.
원문·범위 · §§3.2–3.3, 32–35쪽. skip은 이 글의 무동작 표지.
조건이 이미 false라면 if false then A else B가 고르는 것은?
B입니다. 선택하지 않은 A의 실행을 전제로 요구하지 않습니다.
결정성은 예제 몇 개로 판단할 수 있나요?
결정적이라는 말은 각 구성에서 서로 다른 후속 구성이 최대 하나라는 뜻입니다. 최종값에서는 하나도 없을 수 있습니다. 원문은 작은 식 언어에 대해 구문의 구성 방식으로 귀납합니다. 덧셈의 마지막 규칙이 왼쪽 이동, 오른쪽 이동, 두 숫자 계산 중 무엇인지 나누고 작은 식에 대한 가정을 씁니다.
사회자 유도 나무에 대한 귀납과 구문에 대한 귀납은 어떻게 다릅니까?
답변 구문 귀납에서는 덧셈을 이루는 왼쪽과 오른쪽 식이 더 작습니다. 유도 귀납에서는 마지막 화살표를 정당화한 전제들의 유도가 더 작습니다. 무엇이 작아지는지 적어야 같은 결론을 슬쩍 전제로 쓰는 일을 막을 수 있습니다.
원문·범위 · §3.4, 37–39쪽, 사실 13 및 증명.
초기 구성이 두 후속 구성을 가지지만 끝에서는 모두 10이 되면 결정적인가요?
아닙니다. 그 초기 구성에서 바로 다음 구성이 둘이므로 이미 결정성 조건을 어깁니다.
다음 화살표가 없으면 계산이 끝난 건가요?
정상 종료인지 알려면 최종 집합을 확인합니다. 수 3과 skip은 이 글의 정상 최종 구성입니다. true+3에는 수 덧셈 규칙이 적용되지 않고, 이 식은 최종값도 아니므로 막힘입니다. 원문의 자연수 뺄셈에서도 작은 수에서 큰 수를 빼면 기본 규칙으로 진행할 수 없습니다.
사회자 원문 예제와 true+3은 같은 언어에 있나요?
답변 3.1절 L은 수식과 불식을 문법으로 구분해 자연수 뺄셈을 막힘의 예로 듭니다. true+3처럼 서로 다른 종류의 값을 섞는 식은 3.6절의 확장 언어와 이 글의 교재 모형에서 살핍니다. 이 층위를 구분하면 문법상 만들 수 없는 프로그램을 L의 실행 오류라고 부르지 않게 됩니다.
원문·범위 · §3.1, 29쪽, 정의 11. §§3.5–3.6, 41–43쪽.
오류 규칙을 끈 2−3은 정상 종료일까요?
막힘입니다. 자연수 뺄셈 규칙은 2 ≥ 3을 요구하고, 2−3은 이미 얻은 수가 아닙니다.
PART III · 11–15
오류를 드러내는 규칙과 관찰 범위
막혔다는 것과 오류를 보고했다는 것은 어떻게 다른가요?
기본 뺄셈에서 2−3은 화살표가 없습니다. 오류 보고 규칙을 켜면 2−3 → error라는 화살표 하나가 생깁니다. error는 오류를 보고한 종료 표지이며 정상 숫자값과 구별합니다. 안쪽에서 잘못된 뺄셈을 만났을 때 바깥 연산까지 오류를 전달하는 규칙도 필요합니다.
사회자 5+(2−3)이라는 식을 화면에 넣으면 무엇을 적어야 할까요?
답변 오류 보고가 없을 때에는 안쪽 뺄셈에 전이가 없으므로 전체 식도 막힙니다. 보고 규칙과 전파 규칙을 쓰면 2−3 → error를 전제로 전체가 error로 갑니다. 이 글의 오류 스위치는 자연수 뺄셈에만 오류를 추가합니다. true+3은 스위치를 켜도 막힙니다.
원문·범위 · §3.5, 41–42쪽, 오류 도입·전파 규칙.
2−3에서 ‘후속 구성 하나’와 ‘명시 오류’는 언제 관찰하나요?
첫 구성의 후보는 error 하나입니다. 그 화살표를 따라 도착한 뒤의 상태가 명시 오류입니다.
형 검사를 통과한 계산도 실패할 수 있나요?
형 검사는 실행 전에 조합을 살핍니다. 2+3의 피연산자는 둘 다 nat이므로 결과 형은 nat입니다. true+3은 왼쪽이 bool이어서 이 덧셈의 형을 만들 수 없습니다. 반면 2−3은 두 수라는 형 조건을 만족해도 자연수 뺄셈의 값 조건 2 ≥ 3은 실패합니다.
사회자 형에 맞는지, 끝까지 실행되는지 같은 질문 아닌가요?
답변 검사표에 nat와 nat만 적으면 5−3과 2−3은 같은 줄에 놓입니다. 실제 수를 대입하면 하나는 값 2를 만들고 다른 하나는 오류 보고 규칙으로 갑니다. 반복을 갖는 언어에서는 형에 맞는 반복문도 계속 돌 수 있습니다. 형 검사만으로 종료 여부를 읽을 수 없습니다.
원문·범위 · §§3.5–3.7, 41–46쪽. 3.6절의 nat·bool, 3.7절의 정적 오류.
오류 보고를 끄면 2−3의 정적 형도 바뀌나요?
형은 여전히 nat입니다. 바뀌는 것은 실행에서 막힘으로 남는지 error를 보이는지입니다.
두 규칙이 열려 있으면 어떤 뜻이 생기나요?
화살표는 함수일 필요가 없는 관계입니다. 양쪽 부분식을 모두 먼저 움직일 수 있게 하면 한 구성에서 서로 다른 다음 구성 두 개가 나올 수 있습니다. 이를 비결정적이라고 합니다. 같은 다음 구성을 설명하는 증명이 두 개 있다는 것만으로는 충분하지 않습니다.
사회자 끝에 같은 수가 나오는 두 길도 목록에 모두 남겨야 할까요?
답변 지금 묻는 것은 다음 구성들이므로 둘 다 남깁니다. (1+2)+(3+4)에서 왼쪽을 줄인 식과 오른쪽을 줄인 식은 다릅니다. 한 방향을 고정하면 하나만 남습니다. 실험 3에서 양쪽 허용으로 바꾸고 각 후보를 따라가 보세요. 이 예에서 두 경로가 합류한다는 사실은 다른 모든 프로그램의 합류를 보장하지 않습니다.
원문·범위 · §1.2 정의 1, 4쪽. §3.4 사실 13, 38–39쪽. 양쪽 허용은 비교용.
이미 값 2가 놓인 곳에 오른쪽 우선 규칙을 추가하면 후보가 둘이 되나요?
아닙니다. 값 2에서 나가는 화살표는 여전히 없습니다.
이 규칙으로 만든 대출기는 실제 하드웨어처럼 작동하나요?
이 글에서는 책 수와 승인·거절을 관찰합니다. 카드 판독기 신호, 네트워크 지연, 기록 재시도는 구성에 넣지 않았습니다. 두 기기가 같은 책 수를 같은 새 장부와 화면으로 보낸다면 여기서 정한 관찰로는 구별되지 않습니다. 지연을 비교하려면 시각이나 사건을 구성과 규칙에 추가해야 합니다.
사회자 승인 화면이 같아도 위험한 차이를 알아낼 수 있나요?
답변 어떤 자료를 기록하기로 했는지에 달렸습니다. 처음 세 권의 독자로 시험해 두 장부를 비교하면 옛값을 쓰는 오류가 드러납니다. 반면 화면과 장부가 모두 같아도 네트워크 요청을 두 번 보냈는지는 이 모형에 그 사건이 없으므로 판단할 수 없습니다.
원문·범위 · §1.2, 4–5쪽, 내부·외부 행위와 단계의 크기. §3.2, 31–33쪽.
요청이 두 번 갔는지를 검증하려면 무엇을 추가할까요?
요청 사건을 남기는 로그나 횟수와, 요청을 보낼 때 그것을 갱신하는 규칙이 필요합니다.
이 노트에서 찾은 답을 어디까지 가져갈 수 있을까요?
플롯킨은 덴마크 오르후스대학교에서 강의하며 이 자료를 발전시켰습니다. 1981년 강의노트의 저자 공개본에서 이번에 읽은 부분은 전이 시스템, 식과 명령, 구조적 귀납, 동적 오류와 형 검사입니다. 5장은 선언을, 7장은 함수와 프로시저 등을 더 다룹니다. 서론은 예외와 동시성 같은 주제를 다루지 않았다고 밝힙니다.
사회자 대출기 사례를 다른 프로그램에 옮기려면 제일 먼저 무엇을 적을까요?
답변 지금 남은 구문과 기억할 자료, 정상적으로 끝난 표지를 먼저 정하세요. 다음으로 가장 작은 한 단계를 정해 규칙을 쓰고, 한 번은 규칙이 적용되는 경우, 한 번은 전제가 실패하는 경우를 계산해 보세요. 다룬 예가 몇 개이든 모든 프로그램에 대한 결론을 내릴 때에는 별도 증명이 필요합니다.
원문·범위 · §1.1, 3쪽, 방문·강의와 제외 범위. 목차 1–2쪽, 5·7장.
처음 세 권인 독자 한 명의 성공만으로 모든 구현이 옳다고 할 수 있나요?
그 입력의 기록만 확인했습니다. 가능한 모든 입력과 명령에 대한 주장은 범위를 정하고 증명해야 합니다.
INTERACTIVE NOTEBOOK
전이 규칙을 손으로 시험하기
예상 답을 적고 규칙 하나만 바꿔 보세요. 세 실험은 아래에 적은 작은 언어에서 작동합니다.
EXPERIMENT 01
왼쪽과 오른쪽 중 무엇이 지금 움직일까요?
평가 순서를 고른 뒤 한 단계에 쓸 규칙을 선택하세요. 전제가 맞는 경우에만 아래 기록이 한 칸 늘어납니다.
(1 + 2) + (3 + 4)
왼쪽 우선에서 적용할 첫 규칙은 왼쪽 올리기입니다.
종이로 해 보기 · 왼쪽 우선의 식은 3+(3+4), 3+7, 10 순서입니다.
EXPERIMENT 02
유도 나무의 위와 아래를 맞춰 보세요
장부는 books 한 칸뿐입니다. A와 B는 조건 가지이고 C는 뒤에 남은 명령입니다. 전제 카드와 마지막 규칙을 차례로 고르고, 결론에 남을 장부의 수를 넣으세요.
조건문이 한 단계 움직일 때 장부는 2로 유지됩니다.
종이로 해 보기 · 대입 사례에서 앞 명령이 만든 3을 결론에 그대로 적어야 합니다.
EXPERIMENT 03
후속 구성의 개수로 멈춤과 갈림을 구별하세요
두 피연산자와 규칙을 정하세요. 현재 구성의 판정과 가능한 다음 구성이 모두 나옵니다. 원하는 후보를 선택해 한 번 더 관찰할 수 있습니다.
종이로 해 보기 · 2−3은 기본 규칙에서 막힙니다. 오류 보고를 켜면 다음 구성은 error이고, 그곳에서 명시 오류로 멈춥니다.
원문으로 돌아가는 길
- 고든 플롯킨, 《A Structural Approach to Operational Semantics》. 1981년 오르후스대학교 강의노트 DAIMI FN-19의 저자 공개본입니다. 쪽수는 2004년 1월 30일자 공개본에 인쇄된 쪽을 따릅니다. 1.2절에서 전이 시스템을, 3.1–3.4절에서 규칙과 귀납을, 3.5–3.7절에서 오류·형 검사를 읽었습니다.
- 저자의 연구 목록 17번에서 이 문서를 오르후스 노트의 전자 조판본으로 소개합니다. 플롯킨의 2004년 회고 논문은 1981년 원전의 출처와 강의 배경을 확인하는 데 사용했습니다.
모든 생각그림은 플롯킨의 전이 규칙을 바탕으로 편집부가 구성한 교육용 도해입니다.
한 번의 전이는 두 구성을 잇습니다. 그 한 번을 허용한 근거는 유도 나무에서 찾습니다. 다음 화살표가 끊겼을 때에는 먼저 정상 최종 구성인지 살핍니다.