비결정론적 추상 기계 설계

본 연구는 프로세스 계산이나 완전 비결정론적 베타-환원을 포함하는 람다 계산과 같은 비결정론적 프로그래밍 언어를 위한 추상 기계의 일반적인 설계를 제시한다. 이 기계는 용어를 탐색하여 축약항(redex)을 찾고, 여러 경로가 가능할 때 비결정론적 선택을 수행하며, 더 이상 축약할 수 없는 부분 용어에 도달하면 백트래킹한다. 탐색 과정에서 기계가 도입하는 용어 주석 덕분에 탐색의 종료가 보장된다. 본 연구는 지퍼 의미론(zipper semantics)으로부터 비결정론적 추상 기계를 자동으로 도출하는 방법을 보여준다. 지퍼 의미론은 용어를 문맥과 축약항으로 분해하는 과정을 명시적으로 나타내는 구조적 작동 의미론의 한 형태이다. 도출 방법은 지퍼 의미론에 대한 기계의 건전성(soundness)과 완전성(completeness)을 보장한다. 지퍼 의미론 자체는 순차적 언어, 특히 효과(effect)를 포함하는 언어의 의미론을 기술하는 데 일반적으로 사용되는 환원 의미론(reduction semantics)으로부터 생성될 수 있다. 이러한 설계는 비결정론적 계산 모델의 분석 및 구현을 위한 견고한 기반을 제공하며, 복잡한 언어의 의미론적 특성을 효율적으로 탐색하고 검증하는 데 기여할 수 있다.