MaudeTypedLog: A Typed Interpreter for Prolog in Maude

당신이 카드로 집을 짓고 있다고 상상해 보세요. 컴퓨터 과학의 세계에는 프로로그(Prolog)라는 유명한 언어가 있는데, 이 언어는 마치 숙련된 건축가처럼 행동하지만 매우 느슨한 규칙 책을 가지고 있습니다. 이 건축가는 무거운 벽돌을 섬세한 종이 텐트 위에 올리려고 해도 상관하지 않습니다. 그저 그것들이 서로 맞물리게 하려고 노력할 뿐입니다. 만약 벽돌이 너무 무거우면, 나중에 전체 구조물이 무너지거나, 건축가는 왜 실패했는지 알려주지 않은 채 "음, 이건 안 되겠군"이라고 말하며 그냥 넘어가 버릴 수도 있습니다. 이는 프로로그가 전통적으로 "타입이 지정되지 않았기(untyped)" 때문입니다. 즉, 조각들을 연결하기 전에 그 조각들이 실제로 올바른 모양인지 혹은 재질인지 확인하지 않습니다.

하지만 때로는 건축가가 더 잘 알고 있을 때도 있습니다. 만약 당신이 숫자 리스트를 특정 방식으로 단일 숫자와 섞으라고 요청하면, 건축가는 손을 내저으며 "에러(Error)!"라고 외칠 수도 있습니다. 하지만 이런 일은 이미 건물이 흔들리기 시작한 후에야 일어납니다. 수년 동안 컴퓨터 과학자들은 프로로그에게 더 나은 규칙 책, 즉 "타입 시스템(type system)"을 부여하기 위해 노력해 왔습니다. 즉, 건축을 시작하기 전에 재료를 확인하는 것이죠. 문제는 이러한 시도들의 대부분이 사람들이 사용하기에 너무 복삭잡하거나, 너무 모호해서 명백한 실수조차 놓친다는 점입니다. 이는 마치 지붕만 따로 물어보면 검사하는 안전 검사관이나, 분명히 젤리로 만들어진 벽돌인데도 "아마 벽돌은 괜찮을 것 같다"라고 말하는 검사관과 같습니다.

여기서 새로운 도구가 등장합니다. 연구자 엔리케 갈리파-트론치(Enrique Gallifa-Tronch), 주앙 바르보사(João Barbosa), 산티아고 에스코바르(Santiago Escobar)가 만든 것입니다. 그들은 프로로그를 직접 패치하려고 노력하는 대신, MaudeTypedLog라는 완전히 새로운 엄격한 인터프리터를 만들기로 했습니다. 이 도구는 프로로그의 설계도를 가져와 마우데(Maude)라는 마법 같고 초고속인 시뮬레이션 엔진을 통해 실행하는 것이라고 생각하면 됩니다. 이 엔진은 단순히 조각들을 맞추려고 하는 것이 아니라, 조각들이 서로 닿는 것이 허용되는지조차 확인합니다. 만약 당신이 "숫자"를 "단어"에 붙이려고 한다면, 기계는 즉시 멈춰 서서 "타입 에러(Type Error)!"라고 외칩니다.

이 논문은 이 데 것이 최초로 특정한 '삼항 논리 시스템'을 사용하는 인터프리터임을 제시합니다. 단순히 "예"(작동함) 또는 "아니오"(작동하지 않음)라고 말하는 대신, 이 시스템은 "틀림(Wrong)"(타입 에러임)이라고 말할 수 있습니다. 저자들은 이것이 작동할 것이라고 추측만 한 것이 아니라, 직접 코드를 작성하고 인터프리터를 구축한 뒤 여러 논리 프로그램으로 테스트했습니다. 그들은 이 도구가 다른 도구들이 놓칠 수 있는 명령어(프로그램)와 질문(쿼리) 모두에서 실수를 성공적으로 찾아낼 수 있음을 보여주었습니다. 또한 그들은 이 도구가 단순히 "범죄가 발생했다"라고 말하는 것이 아니라 정확한 용의자를 지목하는 탐정처럼, 문제를 일으키는 특정 코드 라인을 정확히 짚어낼 수 있다는 것을 입증했습니다. 저자들은 자신들의 도구가 아직 완벽하지 않으며 더 많은 테스트가 필요하다는 점을 인정하면서도, 그들의 시뮬레이션은 이 엄격한 방식의 프로그래그램 체크가 오류를 조기에 잡아내는 실행 가능하고 강력한 방법임을 증명했습니다.

MaudeTypedLog의 이야기

문제점: 확인하지 않는 "접착제"
프로로그는 퍼즐이나 논리 문제를 해결하는 데 사용되는 언어입니다. 이는 사실과 규칙의 리스트를 가져와서 질문에 답하기 위해 그것들을 서로 붙이는 방식으로 작동합니다. 전통적으로 프로로그는 "타입이 지정되지 않았습니다." 당신이 양말을 맞추는 게임을 하고 있다고 상상해 보세요. 프로로그에서는 빨간 양말과 파란 신발를 맞추려고 시도할 수 있으며, 게임은 그것이 실패할 때까지 계속 시도합니다. 게임은 "이봐, 그것들은 같은 종류의 물건도 아니잖아!"라고 소리치지 않습니다. 심지어 마지막 순간에도, 그냥 "매칭되지 않음"이라고 말할 뿐, 신발이 문제였다는 설명은 해주지 않습니다.

저자들은 이것이 위험하다고 주장합니다. 때때로 프로그램이 "아니오"라고 말하는 이유는 정말로 답이 "아니오"이기 때문이지만(예: 2는 [1, 3] 리스트에 없음), 다른 경우에는 불가능한 일(예: 단어의 리스트 안에 숫자를 넣는 것)을 시도했기 때문에 "아 아니오"라고 말하는 경우도 있습니다. 프로로그는 이 두 가지를 똑같이 "아니오"로 취급하며, 이는 혼란을 줍니다.

해결책: 삼색 신호등
연구자들은 프로로그 프로그램을 실행하면서 매 단계마다 엄격한 "타입 체크"를 추가하는 인터프리터인 MaudeTypedLog를 구축했습니다. 단순히 초록색(가라)과 빨간색(멈춰라)만 있는 신호등 대신, 이 시스템에는 세 번째 빛인 **노란색(틀림)**이 있습니다.

• 초록색 (참/True): 조각들이 잘 맞고, 타입이 일치하며, 논리가 작동합니다.
• 빨간색 (거짓/False): 타입은 일치하지만, 논리가 작동하지 않습니다 (예: 2는 리스트에 없음).
• 노란색 (틀림/Wrong): 타입이 맞지 않기 때문에 조각들이 결합될 수 없습니다 (예: 단어를 숫자에 더하려고 함).

이 "노란색" 빛이 핵심적인 혁신입니다. 이를 통해 시스템은 프로그램이 나중에 충돌하거나 혼란스러운 답을 내놓기 전에, 타입 에러를 발견하는 즉시 멈출 수 있습니다.

그들은 어떻게 만들었나
이것을 실현하기 위해 저자들은 Maude라고 불리는 강력한 도구를 사용했습니다. 마우데는 규칙을 매우 빠르게 재작성할 수 있는 강력한 시뮬레이션 엔진과 같습니다. 저자들은 프로로그의 규칙을 가져와 마우데 내부에서 재작성했습니다.

1. 타입 지정 유니피케이션(Typed Unification) 알고리즘: 이것이 핵심 엔진입니다. 일반적인 프로로그에서 "유니피케이션(unification)"은 두 가지를 동일하게 만드는 과정입니다. MaudeTypedLog에서, 그들은 "타입 지정 유니피케이션" 알고리즘을 만들었습니다. 두 가지를 붙이기 전에, 그것들의 "타입"을 먼저 확인합니다. 만약 타입이 일치하지 않으면, 단순히 실패하는 것이 아니라 특정 "Wrong" 신호를 반환합니다.
2. TSLD-Resolution: 이것은 그들이 퍼즐을 푸는 데 사용하는 방법의 멋진 이름입니다 (표준 프로로그의 해결 방식인 SLD-resolution의 업그레이드 버전입니다). "T"는 "Typed(타입 지정된)"를 의미합니다. 이것은 문제를 해결하는 모든 가능한 방법의 트리를 구축합니다. 만약 트리의 한 가지 вет(branch)가 "Wrong" 신호에 부딪히면, 그 가지는 즉시 차단되며, 시스템은 어떤 규칙이 오류를 일으켰는지 정확히 알게 됩니다.

그들이 발견한 것
저자들은 몇 가지 예시를 통해 새로운 인터프리터를 테스트했습니다.

• 예시 1: 그들은 r이라는 규칙이 숫자 리스트와 문자 리스트 양쪽 모두에 존재하는 숫자를 찾는 프로그램을 만들었습니다. 시스템은 어떤 경로(숫자 1을 찾는 것)는 작동하지만, 다른 경로(숫자와 문자를 섞으려는 것)는 "Wrong" 신호에 부딪힌다는 것을 정확히 식별해 냈습니다.
• 예시 2: 그들은 숨겨진 타입 에러가 있는 프로그램을 만들었습니다. 한 규칙이 숫자를 위한 자리에 문자를 넣으려고 했습니다. 그들이 "체크" 명령을 실행했을 때, MaudeTypedLog는 단순히 프로그램이 실패했다고 말하는 것이 아니라, 범인인 특정 규칙(clause 3)을 직접 가리켰습니다.

결과는 이 도구가 이론대로 작동함을 보여주었습니다. 이 도구는 프로그램 자체와 프로그램에 던져진 질문 모두에서 타입 에러를 감지할 수 있습니다.

아직 할 수 없는 것
저자들은 현재 작업의 한계를 솔직하게 밝히고 있습니다. 그들의 도구는 프로토타입입니다. 아직 프로로그래밍에서 흔히 쓰이는 모든 복잡한 수학 함수(예: 제곱근 계산이나 동적 숫자 덧셈)를 처리하지 못합니다. 또한 전문적인 프로로그 프로그램들이 사용하는 방대한 규칙 라이브러리에서도 아직 테스트를 거치지 않았습니다. 그들은 향후 이 도구가 이러한 고급 수학 기능과 트리 같은 더 복잡한 데이터 구조를 다룰 수 있도록 가르쳐야 한다고 제안합니다.

왜 중요한가
이 논문은 컴퓨터 과학의 모든 문제를 해결했다고 주장하는 것이 아닙니다. 대신, 논리 프로그래밍을 바라보는 새롭고 더 명확한 관점을 제공합니다. 마우데를 사용하여 엄격한 타입 지정 인터프리터를 만듦으로써, 저자들은 오류를 조기에 포착하고 그것이 발생하는 위치를 정확히 짚어내는 것이 가능하다는 것을 보여주었습니다. 이는 마치 건축가에게 벽이 기울었다고 알려줄 뿐만 아니라, 어떤 벽돌이 잘못된 모양인지도 정확히 알려주어 집이 무너지기 전에 고칠 수 있게 해주는 레이저 수평기를 주는 것과 같습니다.