다섯째 날: 펄은 파싱할 수 없다: 형식적인 증명

저자

Jeffrey Kegler

펄은 파싱할 수 없다: 형식적인 증명

아담 케네디PPI 문서에서 펄의 구문 분석(파싱)은 불가능하다고 추측했습니다. 그리고 이것을 어떻게 증명하는지 보였습니다. 아래에 이 엄격한 형식의 증명을 첨부하였습니다. 여기서 동적 구문 분석과 유사한 이슈는 제외하는 것으로 가정합시다.

저는 이 문제에 호기심을 가지고 있었습니다. 전반적 용도의 파서인 Parse::Marpa의 알파 버전을 CPAN에 배포한 상황이었기 때문이죠. 저는 이것으로 펄 코드의 대부분을 정적 구문 분석을 할 수 있다고 생각했습니다. 그리고 무엇이 가능한지 알고 싶었죠. Parse::Marpa는 어떠한 BNF도 받을 수 있습니다. BNF는 재귀적일 수도 공백의 생성 규칙이나 모호한 규칙을 포함할 수도 있습니다. Marpa를 펄의 구문을 분석하는 것에 사용하면 에드혹 방식의 해결책보다 훨신 덜 불쾌할 것입니다. Parse::Marpa는 LR(0)의 선행 연산 부분과 얼리의 알고리즘을 합치는 새롭게 연구된 방식을 취하여 빠른 속도를 자랑합니다. 특히 유틸리티 목적에 알맞습니다.

이 논란에 처음이신 분들을 위해 말씀드리자면 여기서의 구문 분석, 즉 파스(parse)란 정적인 구문 분석을 의미합니다. 즉, 받은 코드 조각의 구조를 실행하지 않고 결정하는 것입니다. 정적인 구문 분석으로 엄밀하게 보면 펄 프로그램조차 펄의 구문을 분석하지는 않습니다. 펄 프로그램은 펄 코드를 실행하기는 하지만, 이것의 구조를 결정하지는 않습니다. 아담 케네디는 이 논의에서 고려할 사항을 잘 내놓았습니다. 랜달 슈워츠는 이 논의에 중추적인 역할을 했고, 특히 그가 쓴 하나의 펄몽스 게시물이 중요한 역할을 했습니다.

펄의 정적 구문 분석은, 아담 케네디가 보여준 바와 같이, 학문적 호기심 이상의 의미가 있습니다. 자동화된 문서 도구나 Perl::Critic과 같은 분석 도구에도 필요하며, 펄의 표현이나 자동화된 변형을 위해서도 필요합니다.

아래의 증명은 엄격한 계산이론 수준에 달하는 내용입니다. 하지만 펄을 사용하고 펄의 표기법을 사용했습니다. 따라서 수학 저널에 등재할 수는 없을 것입니다. 사실, 그들은 어쨌든 이 글을 받지 않을 겁니다. 라이스의 정리를 자세한 정리 없이 아주 직설적인 순서로 논할 것이기 때문입니다.

정리: 펄 5 구문 분석은 결정 불가능하다

먼저 아담 케네디의 추측을 보조정리로 두겠습니다. 바로 그 뒤에 증명과 정지 문제에 대해 다룹니다.

케네디의 보조정리: 펄의 구문을 분석할 수 있으면, 정지 문제를 풀 수 있다.

케네디의 보조정리를 증명하기 위해, 우리가 펄의 구문을 분석할 수 있다고 가정합니다. 이 가정을 통해, 특히 우리는 랜달 슈와츠가 고안해 낸 다음의 악마같은 코드 조각도 이해할 수 있다고 생각할 수 있습니다.

whatever  / 25 ; # / ; die "this dies!"; 

슈와츠의 코드 조각은 두가지 방법의 구문으로 분석될 수 있습니다. whatever가 어떠한 인자도 받지 않는 연산자(nullary)라면, 첫번째 문장은 공백(void) 문맥에서의 나눗셈 문장이고 남은 부분은 주석입니다. whatever가 인자를 받는다면, 이 코드는 일치 연산자의 반환값을 인자로 받는 whatever 함수를 호출한 뒤 die() 함수를 호출하는 것으로 구문 분석됩니다.

이것이 의미하는 바는, 안정적으로 펄의 구문을 분석하기 위해서는 반드시 어떠한 사용자 함수가 인자를 받는 함수 원형(prototype)인지 아닌지 알아야 한다는 것입니다. 우리가 펄의 구문을 분석할 수 있다고 가정하였으므로, 우리는 이것을 알아낼 수 있는 사용자 함수도 존재한다고 가정합니다. 특히 이 사용자 함수를, 펄 코드를 문자열로 받아서 문자열에 포함된 whatever 함수가 인자를 받지 않는 함수 원형이면 참을 반환하는 is_whatever_nullary() 함수라고 정의합니다.

정지 문제를 도출하기 위해서, 우리는 튜링 기계나 이와 상등한 것으로 모의 실험을 해야 합니다. 펄이 튜링 완전하다는 것은 분명한 사실입니다. 수학 저널의 어떤 심사원도 이렇게 당연한 것을 장황하게 증명하도록 요구하지 않을 것입니다. 이 경우를 전문 용어로 "독자에게 연습 문제로 남긴다"고 합니다만, 우리에겐 Acme::Turing 모듈이 있기 때문에 이미 해결된 것이나 마찬가지로 보이는군요.

우리가 찾은 튜링 기계 모의 실험기를 두 개의 문자열을 인자로 받는 함수로 포장합시다. 첫번째 인자는 튜링 기계의 표현이고 두번째 인자는 튜링 기계의 입력입니다. 이렇게 완성된 run_turing_machin()을 호출합니다.

이번에는 튜링 기계의 설명과 입력을 받는 halts() 루틴을 작성합시다. 우리는 이미 이것을 펄 코드로 만들었습니다. 이 코드는, 우리가 직접 실행하지는 않았지만, 두 개의 인자로부터 기계 표현과 입력 자료를 받는 튜링 기계 모의 실험기를 실행한 후, 인자를 받지 않는 원형을 가지는 whatever 함수를 만듭니다. 그런 다음 is_whatever_nullary()에게 인자를 받지 않는 원형의 whatever 함수가 만들어졌는지 물어봅니다. 우리의 halts() 루틴은 아래와 같을 것입니다.

sub halts {
    my $machine = shift;
    my $input = shift;
    my $code_string_to_analyze = qq{
        BEGIN {
            run_turing_machine("\Q$machine\E", "\Q$input\E");
            sub whatever() {};
        }
    };
    is_whatever_nullary($code_string_to_analyze);
}

$code_string_to_analyzeis_whatever_nullary()의 인자로 전달되면 이것이 어떤 방법으로든 인자가 없는 원형의 whatever 함수가 생성되었는지 알려줄 것입니다. is_whatever_nullary()$code_string_to_analyze를 실행할 필요는 없습니다. 사실 튜링 기계 모의 실험이 끝나지 않으면 is_whatever_nullary$code_string_to_analyze를 실행할 수 없습니다. 또한 함수 원형이 설정되었는지 알려줄 수 있다는 가정에 기댈 수도 없을 것입니다. 따라서, is_whatever_nullary()는 반드시 어떤 방법으로든 언제 $machine$input의 입력으로 정지하지 않는지 알아내야 합니다. $code_string_to_analyze 내부 코드에 인자가 없는 함수 원형의 뒤따라오기 때문에, $machine$input 입력으로 도중에 멈춘다면 is_whatever_nullary는 참을 반환할 것입니다. $machine$input 입력으로 도중에 멈추지 않는다면 인자 없는 함수 원형의 선언에 결국 도달하지 못하고 is_whatever_nullary는 거짓을 반환해야만 합니다.

따라서, 우리가 펄의 구문을 분석할 수 있다고 가정한 것에 의해 halts()는 튜링 기계인 $machine$input 입력으로 멈추는 필요충분한 경우에만 참을 반환합니다. 다르게 말하면, halts()는 정지 문제를 해결합니다. 케네디의 보조정리는, 펄의 구문을 분석할 수 있으면 정지 문제를 풀 수 있다는 것이었습니다. 이것으로 케네디의 보조정리가 증명됩니다.

정지 문제는 판정할 수 없다는 것은 잘 알려진 사실입니다. 케네디의 보조정리가 펄의 구문을 분석할 수 있으면 정지 문제를 판정할 수 있다는 것이 됩니다. 따라서 우리는 펄의 구문을 분석할 수 없습니다.

QED

옮기며

이 글의 원문은 Perlmonks의 Perl Cannot Be Parsed: A Formal Proof이며, 역자는 @am0c입니다. 2008년에 처음 게시되었으며, 정적 파싱 구문에 대해서만 다루므로 지금은 조금 역사적인 의미가 더 크다고 할 수 있습니다. 저자는 이후에 Perl Review에 총 3 파트로 나누어 더 조밀하고 깊게 다루었습니다. perlmonks를 통해 저자에게 해당 노드를 번역하여 달력 기사에 쓸 것은 허락받았습니다. 더 자세한 내용은 원문과 Perl Review의 글을 참고해 주세요.

blog comments powered by Disqus