미국편 · 연재 62PART I · 01–05
대출 장부에서 전부와 하나를 가르다
두 권을 빌린 회원 한 명에서 시작해, 매번 어떤 종료 장부를 조사하는지 따져 봅니다.
대출기의 프로그램은 왜 입력과 출력의 짝으로 그리나요?
대출을 시작할 때마다 장부 한 줄을 복사한다고 생각해 보세요. 이 글의 상태에는 대출 권수 books, 연체 여부 overdue, 처리 상태 status가 있습니다. 처리 상태는 대기·대출·거절 중 하나입니다. 화살표 s→t 하나는 s에서 시작해 t에서 끝나는 실행이 적어도 하나 있다는 뜻입니다. 같은 장부에서 여러 결과를 허용한다면 이 화살표는 여러 갈래가 됩니다.
사회자 2권을 빌린 정상 회원에게 대출도, 대기도 허용하면 어디로 가나요?
답변 한 갈래에서는 책을 더 내주어 (3권, 정상, 대출)로 갑니다. 다른 갈래에서는 장부를 그대로 두어 (2권, 정상, 대기)로 끝납니다. 같은 입력의 두 결과입니다. 어느 경로가 더 자주 선택되는지는 이 관계에 적혀 있지 않습니다.
원문·범위 · §1.1, 인쇄 1–4쪽
결과로 갈 화살표가 둘이면 각각 확률이 절반일까요?
확률은 주어지지 않았습니다. 화살표는 가능한 종료 결과가 무엇인지 알려 줍니다.
호어 삼중항의 약속은 어느 회원에게 적용되나요?
삼중항 {p} α {q}를 확인할 때 먼저 p가 참인 초기 장부만 고릅니다. 그 각각에서 α로 끝나는 결과마다 q가 참이면 약속을 지킵니다. 예를 들어 p를 “정상이며 현재 2권”, α를 새 책 한 권을 내주는 창구, q를 “결과가 3권 이하”로 두세요. 결과는 3권이므로 이 시작 조건에서 약속을 지킵니다.
사회자 처음에 3권인 회원이 4권을 들고 나왔다면 방금 약속이 깨지나요?
답변 위의 p에는 그 회원이 들지 않습니다. p를 “정상이며 3권 이하”로 넓히면 3에서 4로 가는 바로 그 실행이 반례가 됩니다. 앞 조건을 바꾸면 어떤 결과를 검사해야 하는지도 바뀝니다.
원문·범위 · §1.2, 인쇄 5쪽
p를 “정상 3권”으로 바꾼 뒤 q를 그대로 두면요?
창구의 도착값 4는 3 이하여야 한다는 q를 어깁니다. 그 한 쌍이 반례입니다.
상자 [α]q에는 무엇을 남김없이 넣어 보나요?
지금 서 있는 하나의 시작점에서 α의 종료 결과를 전부 꺼내 q를 확인합니다. 2권에서 대출 또는 대기를 선택하면 도착 권수는 3과 2입니다. q가 “3권 이하”일 때에는 두 장부 모두 통과합니다. 상자식의 참은 이 시작점에서 얻은 판정입니다.
사회자 q만 “처리 상태가 대출”로 바꾸면 같은 화살표도 다르게 읽히나요?
답변 3권인 장부는 대출이지만 2권인 장부는 대기입니다. 대기 한 건이 상자식의 반례가 됩니다. 두 경우 모두 실제로 책을 받았다는 뜻으로 상자를 읽으면 바로 이 장부를 지나칩니다.
원문·범위 · §1.1, 인쇄 4쪽
처음 3권인 정상 회원에게 같은 선택을 주면 “3권 이하” 상자는요?
대기면 3권이지만 대출이면 4권입니다. 4권 결과가 있으므로 거짓입니다.
다이아몬드 〈α〉q의 증거는 몇 장이면 되나요?
q인 결과 한 장으로 충분합니다. 3권인 회원이 창구 또는 대기를 선택할 수 있고 q가 “3권 이하”라면 대기를 택한 3권 결과가 증거입니다. 대출해 4권이 되는 실행도 그대로 남습니다. 증거 한 장이 다른 경로를 지우지는 않습니다.
사회자 그 회원이 꼭 창구로 가도록 선택권을 없애면요?
답변 유일한 결과가 4권이 됩니다. 이제 “3권 이하”를 만족하는 종료 결과가 하나도 없어 다이아몬드도 거짓입니다. 결과가 존재한다는 사실과 그 결과가 q라는 사실을 따로 확인해야 합니다.
원문·범위 · §1.1, 인쇄 4쪽
q를 “대출 처리”로 바꾸면 어떤 결과가 증거인가요?
왼쪽 4권 장부입니다. 이번 조건은 권수 대신 처리 상태를 읽습니다.
상자와 다이아몬드를 부정으로 어떻게 맞춰 보나요?
“q인 결과가 하나는 있다”와 “모든 결과가 q를 어기는 것은 아니다”는 같은 말입니다. 이를 〈α〉q ≡ ¬[α]¬q로 씁니다. 여기에 등장하는 모든 결과는 같은 시작점과 같은 프로그램의 결과여야 합니다. 프로그램을 도중에 바꾸면 식 양쪽의 대상도 달라집니다.
사회자 3권·대출과 2권·대기 두 장부에서 q가 대출이라면 안쪽 부정부터 어떻게 읽을까요?
답변 ¬q는 각각 거짓, 참입니다. [α]¬q는 두 값이 전부 참이 아니므로 거짓입니다. 마지막 부정이 이를 참으로 바꿉니다. 한 대출 장부를 직접 찾아 얻은 〈α〉q의 값과 같습니다.
원문·범위 · §1.1, 인쇄 4쪽
모든 종료 결과가 대기뿐이라면 〈α〉대출과 ¬[α]¬대출은요?
두 식 모두 거짓입니다. 대출 장부가 없고 모든 장부가 대출이 아닌 조건을 만족합니다.
PART II · 06–10
길이 끊기거나 서로 이어질 때
거절 한 건과 빈 결과를 구분한 뒤 간선의 합성·선택·반복을 계산합니다.
연체 회원이 차단됐을 때 “모든 결과가 대출”은 참인가요?
차단을 어떻게 기록했는지부터 정해야 합니다. 보통 창구는 연체 신청을 거절 처리하고 끝냅니다. 그 결과는 (2권, 연체, 거절) 한 개입니다. q가 “대출”이라면 그 장부가 반례여서 상자는 거짓입니다. 반면 “정상인가?”라는 시험을 먼저 두고 통과할 때만 다음 일을 하게 하면 연체인 시작점에는 종료 결과가 하나도 없습니다.
사회자 그러면 빈 결과에서도 상자와 다이아몬드 값이 정해지나요?
답변 정해집니다. 결과가 비면 어떤 q에도 상자는 반드시 참입니다. q를 어기는 결과가 없기 때문입니다. 이를 공허한 참이라고 합니다. 다이아몬드는 반드시 거짓입니다. q를 지키는 결과도 없기 때문입니다. 〈α〉참은 별도로 종료 결과가 적어도 하나 있음을 표현합니다. 시험 실패와 무한 반복은 이유가 달라도 결과 관계만 놓고 보면 둘 다 빈 경우가 있습니다.
원문·범위 · §1.1–1.2, 인쇄 4–5쪽 및 §2.1의 시험
빈 결과에서 q를 “4권 이상”으로 바꾸면 상자가 깨질까요?
여전히 참입니다. q의 뜻을 바꿔도 반례로 검사할 종료 결과가 하나도 없습니다.
두 명령을 이어 붙일 때 중간값은 어디에서 만나나요?
실험 2의 작은 계수기는 0·1·2만 허용합니다. α는 1을 더하고 β는 짝수일 때만 통과합니다. 0에서 α를 먼저 실행하면 1입니다. β는 1에서 실패하므로 α;β의 끝은 없습니다. β의 간선 2→2가 보여도 중간값 1과 시작값 2가 다르므로 붙일 수 없습니다.
사회자 이번에는 1에서 출발하면 똑같은 두 명령이 이어질까요?
답변 1→2 뒤에는 2→2를 붙일 수 있습니다. 완성된 경로는 1→2→2이고 전체 프로그램의 시작·끝 쌍은 (1,2)입니다. 식 [α;β]q를 [α][β]q로 읽을 때 이 가운데 상태가 고리 역할을 합니다.
원문·범위 · §1.1 및 §2.2, 합성
0에서 순서를 β;α로 뒤집어 보세요.
짝수 시험이 0→0을 허용하고 증가가 0→1을 허용합니다. 도착은 1입니다.
두 명령 중 하나를 고르면 결과는 어떻게 합치나요?
선택 α∪β에서는 양쪽 관계가 허용하는 간선을 한데 모읍니다. 계수기 0에서 증가를 고르면 1, 짝수 시험을 고르면 0입니다. 두 명령을 순서대로 실행한다는 뜻이 아닙니다. [α∪β]q는 어느 쪽으로 끝나도 q라는 뜻이고, 〈α∪β〉q는 적어도 한 쪽에 증거가 있다는 뜻입니다.
사회자 두 갈래가 둘 다 0에 도착하면 0을 두 번 적나요?
답변 가능한 도착값의 집합에는 0 하나만 있습니다. 서로 다른 명령을 고른 경로는 둘일 수 있으므로 화면은 어느 선택에서 온 간선인지도 적어 둡니다. 결과 집합을 세는 일과 실행 방법을 세는 일은 구별됩니다.
원문·범위 · §2.2, 합집합과 합성
q가 “1이다”면 이 선택에서 상자·다이아몬드는요?
상자는 거짓이고 다이아몬드는 참입니다. 0이 반례이고 1이 증거입니다.
별표 α*에서 한 번도 실행하지 않는 경우가 왜 들어가나요?
α*는 α를 0번 이상 유한하게 반복한 결과를 모읍니다. A→B→C인 복도에서 0걸음이면 A, 1걸음이면 B, 2걸음이면 C입니다. A에서의 도착 집합은 {A,B,C}입니다. 징검다리를 하나 이상 건너야 한다는 다른 약속을 쓰면 A가 빠집니다.
사회자 아무 간선도 없는 곳 D에서 〈α*〉“여기는 D”는 어떻게 되나요?
답변 참입니다. 시작점 D를 그대로 돌려주는 길이 0인 경로가 증거입니다. 그곳에서 〈α〉“여기는 D”는 거짓입니다. 실제 한 걸음을 요구하는데 D에서 나가는 간선이 없기 때문입니다.
원문·범위 · §2.3, 정규 프로그램과 유한 반복
A→B→C에서 정확히 두 걸음의 도착은 어디인가요?
C 하나입니다. 두 걸음 이하라면 A, B, C가 모두 포함됩니다.
도달점 표가 더 늘지 않으면 실제 실행도 반드시 멈출까요?
A→B→C→A인 원을 보세요. A에서 유한하게 도달할 수 있는 점은 A,B,C입니다. 세 점을 기록한 뒤에는 표가 커지지 않습니다. 그러나 기본 프로그램 α의 간선을 계속 고르는 한 실행은 원을 끝없이 돌 수 있습니다. 이 무한한 실행은 α*가 모으는 유한 반복의 종료쌍을 하나 더 만들지 않습니다. 표를 만드는 계산의 종료와 그 표가 묘사하는 모든 실행의 종료는 다른 주장입니다.
사회자 A에서 끝나는 길과 끝나지 않는 길을 함께 허용해도 같은 문제가 생기나요?
답변 그렇습니다. α*에서 0회로 멈춘 A는 종료 결과이고, 고리를 끝없이 도는 과정은 유한 경로의 도착 상태에 한 개를 보태지 않습니다. 〈α*〉참으로는 적어도 하나의 유한 선택을 보일 수 있습니다. 모든 실행이 멈춘다는 전정당성에는 별도의 종료 논증이 필요합니다.
원문·범위 · §2.3, 반복 및 §3.1의 프로그램 모형 비교
점이 네 개라면 전체 도달 관계에 순서쌍이 최대 몇 개 있나요?
4×4=16쌍입니다. 이 상한은 도달점 표의 크기를 제한하며, 실제 실행 길이의 상한은 주지 않습니다.
PART III · 11–15
장부의 어느 칸을 확인할 것인가
대입·시험·관찰의 범위를 바꾸고 계산 결과를 부분정당성의 언어로 다시 읽습니다.
대입에서 무엇이 바뀌고 무엇이 장부에 남나요?
books := books + 1 하나만 실행해 보세요. 오른쪽 식은 갱신 전 장부에서 계산합니다. (2권, 정상, 대기)에서 새 권수는 3이고 나머지 두 칸은 그대로입니다. 창구 프로그램이 새 책을 내주고 상태까지 대출로 바꾸려면 status := 대출도 별도 명령으로 적습니다.
사회자 권수를 바꾸는 대입만 하고 “대출 처리되었다”고 표시하면 무슨 증거가 빠지나요?
답변 바뀐 것은 숫자 칸 하나입니다. 대출 상태를 만들었다는 상태 갱신이 없습니다. 실제 창구 예에서는 두 칸을 모두 바꾸어 (3권, 정상, 대출)이 됩니다. 실험 2의 계수기에서는 2에서 증가하는 간선을 애초에 빼 세 값 안에 머물게 했습니다.
원문·범위 · §2.1, 대입
3권에서 books := books + 1을 두 번 하면 두 번째 오른쪽 값은요?
첫 대입으로 4가 되었으므로 4+1을 계산합니다. 이 문항의 권수에는 계수기 실험의 상한 2가 적용되지 않습니다.
시험은 참과 거짓이라는 값을 돌려주는 명령인가요?
시험 p?를 관계로 쓰면 p가 참인 s에서 s→s만 있습니다. 거짓인 s에서는 간선이 없습니다. 계수기에서 “짝수인가?”는 0→0과 2→2를 허용합니다. 1→거짓이라는 세 번째 값을 만드는 대신 1에서 진행할 결과를 비워 둡니다.
사회자 연체 검사를 하고 반드시 화면에 “거절”을 띄우려면 시험 하나면 될까요?
답변 거절도 하나의 관찰 상태라면 연체일 때 status를 거절로 바꾸는 다른 분기를 두어야 합니다. 시험으로 길을 끊을지, 거절로 끝나는 길을 만들지에 따라 6번 문답의 상자 값이 달라집니다. 실험 1에서 같은 연체 장부를 두 프로그램에 넣어 비교할 수 있습니다.
원문·범위 · §2.1, 시험
p?;p?는 p?와 같은 관계인가요?
그렇습니다. 처음에 참이면 같은 상태에서 두 번째도 참이고 거짓이면 첫 시험에서 더 진행할 결과가 없습니다.
두 장부를 똑같이 읽었다면 프로그램도 같다고 할 수 있나요?
어느 질문을 허용했는지 살펴봐야 합니다. P는 0에서 1로, Q는 0에서 2로 가는 프로그램이라고 합시다. 끝에서 “0보다 큰가?”만 물으면 양쪽 모두 참입니다. 그러나 “짝수인가?”를 물으면 결과 1과 2를 가를 수 있습니다. 제한된 관찰에서 같은 답을 얻었다고 임의의 관계가 같아지는 것은 아닙니다.
사회자 시작점을 0 하나로 고정한 것도 제한인가요?
답변 그렇습니다. 0에서 같은 출력을 내는 두 프로그램도 1에서는 서로 다르게 움직일 수 있습니다. 모든 시작점과 충분한 도착 상태를 구별하는 조건을 갖추면, 특정 쌍 (s,t)가 관계에 있는지를 묻는 방식으로 차이를 드러낼 수 있습니다.
원문·범위 · §1.2 및 §3.1, 프로그램 기술과 관찰 범위
실험에서 몇 개의 조건값이 같았으면 모든 프로그램식에서도 같을까요?
그 조건들과 입력에서 같음을 확인한 것입니다. 허용한 관찰 언어와 전체 시작점에 대한 별도 논증이 필요합니다.
호어의 증명 규칙과 프랫의 관계 그림을 어떻게 함께 읽나요?
39편은 프로그램에 붙인 앞·뒤 조건을 증명 규칙으로 잇는 법을 다뤘습니다. 여기서는 주어진 관계에서 그 조건이 실제로 참인지 따집니다. 모든 시작점에서 p→[α]q라는 식이 참이면 관계적 부분정당성의 {p} α {q}가 성립합니다. 중간 조건 r을 찾아 두 명령의 증명을 잇는 일과, 가운데 상태 u를 찾아 두 간선을 잇는 일이 어떻게 맞물리는지도 비교할 수 있습니다.
사회자 0에서 증가한 뒤 짝수만 통과시키는 명령은 도착점이 없는데, 부분정당성은 어떻게 읽죠?
답변 앞 조건을 x=0이라 두면 이 합성에서는 어기는 종료 상태가 없어 어떤 뒤 조건에도 부분정당성이 성립합니다. 그렇지만 도달 가능한 결과를 요구하는 〈α〉참은 거짓입니다. 증명하려는 사양에 최소 한 번의 종료가 필요한지 먼저 적어야 합니다.
원문·범위 · §1.2 및 §2.2, 부분정당성과 합성
적어도 한 실행이 종료한다면 모든 실행도 종료할까요?
둘은 다릅니다. 한 갈래가 종료하고 다른 갈래가 끝없이 이어질 수 있습니다.
이 모형으로 프랫의 원문 어디까지 확인했나요?
한 번의 대출과 세 칸의 계수기로 프로그램의 결과 관계를 열거했습니다. 그 관계에서 모든 결과와 어떤 결과를 따져 상자와 다이아몬드를 계산했고, 합성·선택·유한 반복의 뜻을 확인했습니다. 원전은 이런 관점에서 프로그램에 관한 기술의 참과 그 참을 증명하는 규칙의 관계를 연구합니다.
사회자 작은 실험 표가 전부 녹색이면 동적 논리 전체의 완전성까지 확인한 걸까요?
답변 실험은 입력한 유한 관계의 답을 구합니다. 증명 체계의 완전성은 해당 언어에서 의미론적으로 참인 모든 식을 규칙으로 증명할 수 있는지에 관한 명제입니다. 프랫은 1976년 보고서에서 반복문이 없는 양상 프로그램 체계의 완전성을 구분해 설명합니다. 지금 손으로 세어 본 경로는 그런 정리의 증명이 아닙니다.
원문·범위 · 초록, §1 및 §3의 양상 접근
다음 독자에게 이 글의 관찰법을 한 문장으로 설명해 보세요.
어느 상태에서 출발해 어떤 실행이 끝났는지 먼저 적고, 조건을 만족해야 하는 것이 전부인지 하나인지 정합니다.
FIELD NOTES
옆에 두고 읽는 여섯 기호
- s Rα t
- 프로그램 α의 한 종료 실행이 시작 상태 s에서 도착 상태 t로 갑니다.
- [α]q
- 현재 상태에서 α의 모든 종료 결과가 q를 만족합니다. 결과가 비면 참입니다.
- 〈α〉q
- 현재 상태에서 α의 종료 결과 중 하나 이상이 q를 만족합니다. 결과가 비면 거짓입니다.
- α;β
- α의 도착점과 β의 출발점이 일치하는 경로를 이어 붙입니다.
- α∪β
- α와 β 가운데 어느 쪽에서 허용한 간선이든 관계에 넣습니다.
- α*
- α를 0번 이상 유한하게 반복한 끝을 모읍니다. 0회로 처음 상태도 포함합니다.
INTERACTIVE NOTEBOOK
장부와 화살표를 직접 바꿔 보기
결과를 예상한 다음 선택을 하나 바꾸세요. 세 실험은 서로 다른 상태 공간을 사용하며 모든 계산을 이 브라우저에서 수행합니다.
1. 대출이 거절된 것과 결과가 없는 것
연체 회원과 창구 처리를 고른 뒤, 프로그램만 정상 시험으로 바꿔 보세요. 두 결과에서 대출 권수·연체 여부·처리 상태를 모두 표시합니다.
2. 어디에서 두 명령을 잇나요?
계수기 값은 0·1·2입니다. 증가·감소가 범위를 벗어나면 그 간선이 없습니다. 0에서 증가와 짝수 시험을 합성한 뒤 순서를 바꿔 보세요.
3. 유한 반복 표 만들기
먼저 시작점만 적고 한 걸음 간선을 거듭 따라갑니다. 새로 만난 점의 처음 횟수를 기록합니다. 화면의 횟수는 정확히 그만큼이 아니라 그 이하입니다.
원문의 위치와 읽은 범위
- MIT Laboratory for Computer Science 기술보고서 TR-168. 1976년 9월. 1절에서 프로그램·양상·부분정당성의 관계 해석을, 2절에서 시험·대입·합성·선택·반복을 읽었습니다. 3절과 초록은 언어와 공리계의 범위를 정할 때 참고했습니다.
- IEEE 제17회 FOCS 학회 판본. 1976년, 학회 논문집 109–121쪽. 이 글은 학회지 쪽수와 MIT 보고서 쪽수를 구별합니다.
- 같은 연재 39편 · 호어의 프로그램 증명. 앞·뒤 조건을 잇는 증명 규칙에서 이번 편의 종료 관계로 이어 읽을 수 있습니다.
거절이라고 끝난 장부가 한 장 있는지, 도달한 장부가 정말 없는지 먼저 세어 보세요. 같은 “대출되지 않았다”는 말 아래에도 상자식의 참값을 갈라놓는 차이가 있습니다.