동작 기록이 같아도, 선택의 갈림길이 다르면 같은 과정일까요?

점은 지금 할 수 있는 일이 정해져 있는 상태입니다. 화살표의 글자는 한 번 수행하는 관찰 동작입니다. P에서 a 화살표가 두 갈래로 나가는 것은, 같은 입장 확인 동작 뒤에 서로 다른 두 상태가 가능하다는 뜻입니다. 화살표가 두 개라는 사실로 각각 선택될 확률까지 알 수는 없습니다.

동작 a를 한 뒤 과정 X를 계속하는 것을 a·X로 쓰겠습니다. X+Y는 X 또는 Y의 가능한 동작을 선택하는 과정입니다. 아무 동작도 더 하지 않는 상태는 0으로 쓰겠습니다. 그러면 P=a·(b·0)+a·(c·0), Q=a·(b·0+c·0)입니다. 읽기 편하게 뒤의 ·0은 줄여 쓰기도 하겠습니다.

P에서는 a를 수행하는 전이를 고르면서 이후의 가능성이 b 또는 c로 좁아집니다. Q는 a 뒤에도 두 가능성을 유지합니다. 이것은 이 모형이 구별하는 선택의 시점입니다. 물리 장치 속에서 어떤 부품이 실제로 먼저 움직였는지까지 이 식에 담았다는 뜻은 아닙니다.

흔적(trace, 수행한 동작을 순서대로 적은 기록)은 중간에 멈춘 기록까지 포함하도록 정할 수 있습니다. 이 글에서는 아무 동작도 하지 않은 빈 기록 ε, 입장만 확인한 a, 두 동작을 마친 ab와 ac를 모두 흔적으로 셉니다. 따라서 두 안내기의 흔적 집합은 각각 {ε, a, ab, ac}입니다.

한편 더 진행할 동작이 남지 않은 끝 상태에 도달한 기록만 모으면 완료 흔적 집합 {ab, ac}가 됩니다. 앞의 도입에서 나란히 놓은 두 줄은 이 완료 흔적이었습니다. 흔적과 완료 흔적을 같은 이름으로 부르면, 중간 상태를 포함했는지가 흐려집니다.

지금은 두 집합 모두 P와 Q에서 같습니다. 그래도 a를 수행한 뒤 어떤 선택지가 함께 남는지는 그 집합에 기록되어 있지 않습니다. ab가 가능하고 ac가 가능하다는 정보는, 같은 a 뒤의 한 상태에서 b와 c가 모두 가능한지를 따로 말해 주지 않습니다.

두 상태를 한 쌍으로 놓고 한쪽에서 가능한 동작을 고릅니다. 그 동작을 다른 쪽에서도 수행할 수 있어야 하며, 동작 뒤의 두 상태도 다시 비교할 쌍으로 남아야 합니다. 출발점에서 동작 이름이 같다는 확인만으로 검사가 끝나지 않습니다.

이 요구는 양쪽 방향에 모두 적용합니다. 왼쪽의 모든 동작에 오른쪽의 대응이 있고, 오른쪽의 모든 동작에도 왼쪽의 대응이 있어야 합니다. 왼쪽에는 없는 기능을 오른쪽이 추가로 제공한다면 한쪽 검사만 통과하고 반대쪽에서 실패할 수 있습니다.

이처럼 계속 서로의 동작을 맞추는 상태 관계를 이 글에서는 쌍방 모사 관계, 바이시뮬레이션(bisimulation)이라고 부릅니다. 원전은 관찰 관계를 바탕으로 단계별 동치를 정의하고, 각 상태의 동작별 후속 상태가 유한하다는 조건에서 고정점으로 설명합니다. 아래의 유한 안내기에서는 그 조건을 직접 확인할 수 있습니다.

P가 a를 수행해 Pb로 이동했다고 합시다. Q에서 같은 a를 수행하면 도착할 수 있는 상태는 Qbc 하나입니다. 따라서 P와 Q를 계속 같은 것으로 보려면 Pb와 Qbc를 짝지어야 합니다.

Pb의 b는 Qbc의 b와 맞출 수 있습니다. 둘 다 동작 뒤에 끝 상태 0으로 갑니다. 그러나 반대쪽에서 Qbc의 c를 고르면 Pb에는 c 전이가 없습니다. 두 상태는 서로의 동작을 모두 맞추지 못합니다.

P가 다른 a 전이를 골라 Pc로 가도 상황은 대칭적입니다. 이번에는 Qbc의 b를 맞출 수 없습니다. Q의 a 후속 상태를 다른 것으로 바꾸어 피할 수도 없습니다. 그 상태가 하나뿐이기 때문입니다. 그래서 출발점 P와 Q 역시 쌍방 모사 동치가 되지 않습니다.

〈a〉φ는 a를 한 번 수행한 뒤 조건 φ를 만족하는 상태로 갈 수 있다는 뜻으로 사용하겠습니다. ⊤는 어떤 상태에서나 참인 조건입니다. 따라서 〈b〉⊤는 b 동작이 가능하다는 말이고, 〈c〉⊤는 c 동작이 가능하다는 말입니다.

이제 〈a〉(〈b〉⊤ ∧ 〈c〉⊤)를 읽어 보겠습니다. ‘a를 수행한 뒤, b도 가능하고 c도 가능한 한 상태에 도달할 수 있다’입니다. Q는 Qbc로 가므로 이 조건을 만족합니다. P의 두 a 후속 상태는 각각 한 동작만 가능하므로 이 조건을 만족하지 않습니다.

괄호 안의 ∧가 같은 후속 상태에 두 요구를 함께 거는 데 주목해 주세요. 〈a〉〈b〉⊤ ∧ 〈a〉〈c〉⊤는 a를 통한 두 가능성을 따로 고를 수 있어서 P와 Q가 모두 만족합니다. 괄호가 놓인 위치가 관찰의 질문을 바꿉니다.

출발점만 놓고 가능한 다음 동작 이름을 보면 P와 Q 모두 a를 제공합니다. 한 단계 검사에서는 둘을 구별하지 못합니다. 두 번째 단계에서 a 뒤의 동작들을 맞추려고 하면 b와 c의 차이가 드러납니다.

원전은 아무것도 구별하지 않는 단계에서 시작하여 관찰 깊이를 하나씩 늘리는 관계를 정의합니다. 다음 단계에서는 같은 동작 뒤의 상태들이 이전 단계에서 여전히 한 쌍인지 확인합니다. 앞 단계에서 실패한 상태 쌍을 이용하면 그 쌍으로만 대응할 수 있었던 출발점도 뒤이어 탈락합니다.

우리 실험은 유한한 상태 쌍의 목록을 만들고, 맞출 동작이 없는 쌍을 반복해서 제거합니다. 한 번에 제거할 쌍을 모은 뒤 다음 라운드로 넘어가므로, 계산 순서 때문에 결과가 바뀌지 않습니다. 더 이상 제거할 쌍이 없을 때 남은 관계를 확인합니다.

현재 모형에서 두 상태가 계속 서로의 동작을 맞출 수 있다면, 〈a〉 같은 관찰 조건도 같은 방식으로 만족해야 합니다. 왼쪽에 조건을 만족하는 a 후속 상태가 있으면 오른쪽에서 대응 후속 상태를 찾을 수 있고, 그 뒤 조건도 다시 비교할 수 있기 때문입니다.

원전의 정리 2.2는 각 동작에 대한 후속 상태가 유한한 관찰 관계에서, 관찰 동치와 해당 양상 언어로 표현할 수 있는 모든 성질의 일치를 연결합니다. 여기서 ‘모든’은 몇 가지 우리가 골라 본 식을 뜻하지 않습니다. 논문이 정의한 언어의 식 전체를 가리킵니다.

이번 안내기에서는 두 상태를 구별하는 구체적인 식 하나를 이미 찾았습니다. 따라서 그 식에 관한 참·거짓 계산만으로 P와 Q의 차이를 설명할 수 있습니다. 실험에 들어 있는 세 식이 우연히 같은 결과를 낸다는 사실만으로 임의의 두 과정을 동치라고 결론 내리지는 않습니다.

모형을 만들 때 먼저 관찰자가 무엇을 구별하는지 정합니다. 화면에 입장 완료가 뜨는 일과 장치 내부 메모리 정리는 서로 다른 관찰 수준일 수 있습니다. 모두 눈에 보이는 동작처럼 취급하면 내부 구현 차이도 그대로 드러납니다.

내부 동작을 숨기고 그 전후의 관찰 가능한 행동을 비교하려면, 내부 동작을 거칠 수 있는 경로를 포함하는 별도의 관찰 관계가 필요합니다. 동작 이름을 지웠다는 이유만으로 앞서 사용한 한 단계 대응 계산과 같은 의미가 되는 것은 아닙니다.

이 글의 세 실험은 a·b·c·d를 모두 관찰 가능한 동작으로 두고, 내부 동작을 포함하지 않습니다. 따라서 화면의 동치 판정은 이 공개된 유한 전이계에 대한 결과입니다. 논문 후반의 내부 동작과 관찰 합동관계는 다음 질문에서 범위를 구분해 읽겠습니다.

어떤 조각 X 앞에 동작 d를 붙인 d·X를 생각해 봅시다. 원래 두 조각이 서로의 관찰 동작을 맞출 수 있다면, d를 수행한 뒤에도 원래의 대응 관계를 이어 쓸 수 있습니다. 이처럼 조각을 둘러싸는 구조를 문맥(context, 프로그램 조각이 들어가는 주변 구조)이라고 부릅니다.

관찰 규칙과 언어를 바꾸면 모든 문맥에서 이런 보존이 저절로 따라오는 것은 아닙니다. 논문은 관찰 동치와 문맥 속의 치환을 구별해 다루고, 합동관계라는 요구를 따로 검토합니다. 어떤 연산을 허용하는지와 어떤 관찰 관계를 쓰는지 함께 적어야 합니다.

아래 실험은 내부 동작 없는 유한 과정에서 접두사 d와 공통 선택지 e를 더합니다. 이것은 해당 제한된 문맥의 계산입니다. 모든 언어·모든 숨은 동작·모든 실행환경에서 치환이 안전하다는 일반 보증으로 확대하지 않습니다.

우리가 쓰는 +는 가능한 동작들의 선택을 나타냅니다. b·0+c·0와 c·0+b·0는 각각 b와 c를 수행한 뒤 끝 상태로 갑니다. 식에 b를 먼저 적었다고 먼저 실행되는 우선순위를 주지 않았습니다.

두 시작 상태를 짝짓고 끝 상태끼리 짝지으면 됩니다. 왼쪽 b는 오른쪽 b, 왼쪽 c는 오른쪽 c와 대응합니다. 오른쪽에서 시작해도 같은 확인이 가능합니다. 그러므로 이 두 유한 과정은 쌍방 모사 동치입니다.

실제 프로그래밍 언어의 if와 else if처럼 앞 조건을 우선 검사하는 문법을 여기에 대입하면 의미가 달라집니다. 기호 +가 어떤 선택을 뜻하는지 정한 뒤에 교환 법칙을 적용해야 합니다. 같은 기호처럼 보여도 언어의 실행 규칙은 먼저 읽어야 합니다.

우리의 관찰 관계는 어떤 상태로 갈 수 있는지를 기록하는 관계입니다. 같은 b 동작으로 같은 끝 상태에 가는 전이를 두 번 적어도, 갈 수 있는 상태의 집합은 바뀌지 않습니다. 이 의미에서는 b·0+b·0와 b·0를 대응시킬 수 있습니다.

관찰자가 동작의 발생 확률이나 자원 비용까지 재도록 모형을 바꾸면 검토할 정보가 늘어납니다. 지금은 전이를 추첨권처럼 세거나, 중복된 선에 서로 다른 확률을 부여하지 않았습니다. 그래서 같은 선택의 반복을 하나로 정리하는 멱등 법칙을 적용할 수 있습니다.

실험의 세 번째 비교에서 이 두 과정을 선택하면 동치가 표시됩니다. 이어 P와 Q로 바꾸면 동치가 깨집니다. 둘 다 식을 짧게 정리하는 모양으로 보이지만, 앞서 관찰한 분기 구조가 실제로 보존되는지를 각각 계산해야 합니다.

숫자 계산의 분배 법칙에 익숙하면 a·(b+c)를 a·b+a·c로 바꾸고 싶어집니다. 그러나 이 글의 ·는 곱셈을 뜻하지 않고, 앞 동작을 수행한 뒤 다음 과정을 계속한다는 뜻입니다. 같은 기호 모양만으로 산술 법칙을 가져올 수는 없습니다.

이미 두 안내기에서 답을 구했습니다. a·(b+c)는 Q이고 a·b+a·c는 P입니다. Q에서는 한 번의 a 뒤에 b와 c가 함께 남지만 P에서는 각 a 뒤에 하나만 남습니다. 따라서 이 전개는 이 글의 쌍방 모사 의미에서 동치를 보존하지 않습니다.

완료 흔적만 비교하는 목적이라면 두 식의 {ab,ac}는 같습니다. 목적에 따라 같은 변형을 허용할 수도 있고 금지할 수도 있습니다. 어느 동치를 지키려는지 먼저 적으면 ‘기호를 잘 전개했다’와 ‘프로그램의 필요한 성질을 보존했다’를 구분할 수 있습니다.

실험에 등장하는 상태가 N개라면 비교 후보는 순서 있는 상태 쌍 N²개입니다. 반복 계산은 후보를 지우기만 하고 다시 추가하지 않습니다. 어떤 라운드에 하나라도 지워졌다면 후보 수가 줄므로, 유한 번 뒤에는 더 지울 쌍이 없는 상태에 도달합니다.

이 종료 설명은 우리가 화면에 만든 유한 전이계에 적용됩니다. 임의의 프로그램에는 무한히 많은 상태가 있거나, 입력에 따라 계속 새로운 값이 생길 수 있습니다. 그런 프로그램까지 유한 표 하나로 다 검사했다고 볼 수는 없습니다.

원전의 일반 결과에서 필요한 조건과 실험 구현의 종료 조건도 따로 적습니다. 동작별 후속 상태가 유한하다는 조건은 전체 상태 수가 유한하다는 조건과 다릅니다. 이번 모형은 전체 상태가 유한하므로 더 강한 조건을 만족하고, 유한 표 제거 절차를 사용할 수 있습니다.

먼저 비교하려는 관찰을 적습니다. 입장 확인과 방 안내만 볼 것인지, 응답 시간과 오류 메시지도 볼 것인지에 따라 상태와 동작의 목록이 달라집니다. 이번 글에서는 a·b·c의 수행 가능성만 관찰했습니다.

다음으로 차이를 보여 준 경로와 조건을 함께 남깁니다. P에서 a 뒤 Pb로 가면 c를 수행할 수 없고, Q에서 a 뒤 Qbc로 가면 c를 수행할 수 있다는 기록이 그런 근거입니다. 이를 〈a〉(〈b〉⊤ ∧ 〈c〉⊤)의 참·거짓 표로도 확인했습니다.

마지막으로 사용한 모형의 범위를 기록합니다. 이번 결론은 숨은 동작·확률·시간을 포함하지 않은 두 유한 안내기에 관한 것입니다. 새로운 관찰이 필요해지면 상태와 전이를 보완하고 다시 비교할 수 있습니다. 완료 기록만 보던 처음 질문이, 중간에 남아 있는 선택지까지 확인하는 질문으로 깊어진 것입니다.