Barbed Similarity for the $\pi$-Calculus in Beluga: A Case Study in Coinductive Reasoning

당신이 아주 작은 투명 로봇인 "프로세스(process)"들이 등장하는 영화를 보고 있다고 상상해 보세요. 이 로봇들은 서로 대화하고, 비밀 노트를 주고받고, 심지어 영원히 자신을 복제할 수도 있는 혼란스러운 도시에서 살고 있습니다. 이 이야기 속 과학자들의 거대한 질문은 이것입니다: 두 로봇이 정말로 똑같이 행동하고 있다는 것을 어떻게 알 수 있을까요?

만약 로봇 A와 로봇 B가 겉모습은 다르지만, 가능한 모든 상황에서 정확히 똑같은 행동을 한다면, 그들은 "유사(similar)"하다고 합니다. 하지만 이를 증명하는 것은 유령을 잡으려는 것과 같습니다. 그들이 단 한 번이라도 실수하는 모습을 포착하기 위해, 당신은 모든 가능한 동네에서, 모든 가능한 친구들과 함께 그들을 지켜봐야 합니다.

이 논문은 레아 트로니(Lea Trogni), 가브리엘레 체칠리아(Gabriele Cecilia), 알베르토 모밀리아노(Alberto Momigliano)가 집필한 이 로봇들에 관한 3부작 영화의 마지막 장입니다. 그들은 **벨루가(Beluga)**라는 초지능적인 컴퓨터 조수를 사용하여, 논리적 오류가 발생하지 않도록 보장하는 기계 검증된 대본과 같은 증명을 작성했습니다.

반전: "복제" 문제

이 이야기의 이전 장들에서, 과학자들은 이 로봇들이 움직이는 규칙 책을 가지고 있었습니다. 하지만 그들은 "복제(replication)"라고 불리는 버튼에 대한 아주 작고 결정적인 세부 사항을 놓쳤습니다.

"나는 영원히 나 자신을 복제하겠다!"라고 말하는 로봇을 상상해 보세요. 예전의 규칙 책 아래에서는, 원래 동일해야 할 두 로봇에게 이 복제 버튼을 주면 컴퓨터 조수가 "잠깐, 이 둘은 실제로 같지 않습니다!"라고 말할 것입니다. 이는 이 로봇들의 세계에서, 자신을 복제할 수 있다는 사실이 equality(동등성)의 규칙을 깨뜨려서는 안 되기 때문에 문제가 되었습니다.

저자들은 이 실수(약간은 당혹스러운 설정 오류)를 깨닫고 이를 수정했습니다. 그들은 복제된 존재들이 통신하는 방식에 특화된 두 가지 새로운 규칙을 대본에 추가했습니다. 일단 그렇게 하자, 이야기는 다시 말이 되었습니다. 이는 완벽한 대본을 가지고 있다고 생각할 때조차도, 기계가 인간이 놓칠 수 있는 미세한 오류를 잡아낼 수 있음을 보여줍니다.

탐정 작업: "바브드(Barbed)" 유사성

그렇다면 우리는 두 로봇이 같다는 것을 어떻게 알 수 있을까요? 저자들은 **바브드 유사성(Barbed Similarity)**이라는 개념을 사용합니다.

"바브(barb)"를 특정 거리로 손을 내밀어 흔드는 로봇의 손짓이라고 생각해 보세요.

• 만약 로봇 A가 "메인 스트리트"를 향해 손을 흔든다면, 로봇 B 역시 "메인 스트리트"를 향해 손을 흔들 수 있어야 합니다.
• 만약 로봇 A가 자기 자신에게 비밀을 속삭인다면(내부 동작), 로봇 B도 똑같이 할 수 있어야 합니다.

저자들은 두 로봇이 서로의 손짓과 속삭임이 일치한다면, 그들이 "유사"하다는 것을 증명했습니다. 하지만 까다로운 점은 여기 있습니다: 유사성이 항상 모든 상황에서 교체 가능하다는 것을 의미하지는 않는다는 것입니다.

로봇 A와 로봇 B가 모두 유사하다고 가정해 봅시다. 하지만 당신이 특정 동네(컨텍스트)에 그들을 배치하면, 로봇 A는 갑자기 로봇 B는 도달할 수 없는 새로운 거리를 향해 손을 흔들기 시작할 수도 있습니다. 저자들은 유사성 규칙을 충분히 엄격하게 만든다면—즉, 추가적인 친구를 더하거나 이름을 바꾸었을 때의 행동까지 체크한다면—그들이 **프리컨그루언트(precongruent)**해진다는 것을 증명해야 했습니다. 이것은 "그들은 매우 유사해서, 어디에서든 서로 교체해도 세상이 눈치채지 못할 정도이다"라는 것을 뜻하는 멋진 표현입니다.

마술 기법: "Up-to" 기법

이를 증명하기 위해 저자들은 "up-to" 기법이라는 마술을 사용했습니다.

당신이 두 줄의 긴 도미노가 똑같이 쓰러질 것임을 증명하려고 노력하고 있다고 상상해 보세요. 모든 도미노가 하나씩 쓰러지는 것을 일일이 지켜보는 대신(그러려면 영원히 걸릴 것입니다), 당신은 이렇게 말합니다. "음, 이 처음 몇 개가 똑같이 쓰러지고, 나머지 부분은 이미 유사하다고 증명되었으므로, 전체 라인도 똑같이 쓰러져야 해."

저자들은 이 기법을 사용하여 증명을 훨씬 더 짧고 깔끔하게 만들었습니다. 그들은 몇 가지 핵심적인 움직임을 확인하는 것만으로도, 수백만 줄의 코드를 작성하지 않고도 전체 시스템이 작동한다는 것을 증명하기에 충분하다는 것을 보여주었습니다.

판결: 그들은 실제로 무엇을 증명했는가?

저자들은 단순히 추측한 것이 아니라, 벨루가 내부에서 **형식적 증명(formal proof)**을 구축했습니다. 즉, 컴퓨터가 그들의 논리적 단계를 하나하나 체크했다는 뜻입니다.

• 결과: 그들은 이 특정 로봇들($\pi$-calculus와 복제 기능이 있는 경우)에 대해, 그들의 "손짓(barbs)"과 내부 움직임을 확인하면, 그것을 어떤 상황에서도 작동하는 규칙으로 바꿀 수 있다는 것을 성공적으로 증명했습니다.
• 확신: 그들은 자신들이 작성한 논리에 대해 100% 확신하는데, 그 이유는 컴퓨터가 이를 검증했기 때문입니다. 다만, 이 특정 논문에서는 역방향(만약 그들이 교체 가능하다면 반드시 바브드 유사해야 하는가)은 증명하지 않았음을 인정합니다. 그들은 이를 미래의 연구를 위한 "속편"으로 남겨두었습니다.
• 규모: 전체 증명은 약 1,500줄의 코드로 이루어져 있습니다. 여기에는 23개의 정의와 53개의 정리가 포함됩니다. 이는 방대한 백과사전은 아니지만, 매우 견고하고 적절한 규모의 프로젝트이며 이론의 가장 중요한 부분들을 다룹니다.

이것이 왜 중요한가

이 논문은 HOAS(Higher-Order Abstract Syntax)를 사용하는 것이 마치 초능력을 갖는 것과 같다고 주장합니다. 다른 언어들에서는 로봇의 이름(예: "이름 A", "이름 B")을 수동으로 관리하고 서로 섞이지 않도록 주의해야 합니다. 하지만 벨루가에서는 컴퓨터가 이름을 자동으로 처리해 줍니다. 이는 코드를 훨씬 짧게 만들고 인간의 실수 가능성을 낮춰줍니다.

그들은 또한 코인덕션(coinduction)(무한한 행동을 증명하는 데 사용되는 방법)이 벨루가에서 아름답게 작동한다는 것을 발견했습니다. 이는 마치 무한 루프에 빠지지 않고도 무한 루프에 대해 증명할 수 있게 해주는 도구를 가진 것과 같습니다.

그들이 하지 않은 것 (그리고 그것이 중요한 이유)

논문은 초점을 유지하기 위해 몇 가지 사항을 명시적으로 제외했습니다:

• 그들은 대칭적인 경우(로봇 B가 로봇 A와 유사한지 확인하는 경우)를 증명하지 않았습니다. 왜냐하면 그것은 이미 수행한 작업의 복사 붙여넣기에 불과하기 때문입니다. 그들은 이를 자동화의 영역으로 남겨두었습니다.
• 그들은 "생산성 체크 도구(productivity checker)"(무한 루프가 안전한지 자동으로 확인하는 안전망)를 사용하지 않았습니다. 벨루가에 아직 해당 기능이 없기 때문입니다. 대신, 그들은 모든 단계가 안전한지 수동으로 확인했습니다.
• 그들은 "컨텍스트 렘마(Context Lemma)"의 역방향을 해결하지 않았습니다. 그들은 유사하다면 교체 가능하다는 것을 증명했지만, 교체 가능하다면 반드시 유사해야 한다는 것을 증명하지는 않았습니다.

결론

이 논문은 복잡하고 무한한 세계의 논리를 검증하기 위해 컴퓨터를 사용하는 성공 사례입니다. 저자들은 규칙 책의 작은 버그를 수정했고, 증명을 단축하기 위해 영리한 마술 기법을 사용했으며, 이 방법이 까다로운 복제 로봇들을 다루는 데 훌륭한 방법임을 보여주었습니다.

그들은 단지 이것이 작동할 것이라고 제안한 것이 아니라, 그들의 특정 설정 내에서 그것이 작동함을 증명했습니다. 비록 미래의 시리즈를 위한 몇 가지 미해결 과제들이 남아있지만, 이 장은 매우 중요한 퍼즐 조각의 고리를 닫았습니다.