흥미로운 질문이 있습니다. 그러나 정확히 어떻게 구절을 사용해야하는지 잘 모르겠습니다 ...최적의 처리 순서를 찾는 방법은 무엇입니까?
람다 계산법을 고려하십시오. 주어진 람다 식에서 몇 가지 가능한 축소 명령이 있습니다. 그러나 이들 중 일부는 종료되지 않으며 다른 일부는 종료됩니다.
람다 미적분학에서 하나의 특정 축소 순서가 있음이 밝혀졌습니다. 보장 된은 실제로 존재할 경우 기약 해결책으로 종결됩니다. 그것은 보통 명령이라고 불립니다.
간단한 논리 해결사를 작성했습니다. 그러나 문제는 제약 조건을 처리하는 순서가 솔루션을 찾았는지 아닌지에 큰 영향을 미친다는 것입니다. 기본적으로, 나는 나의 논리 프로그래밍 언어에 대한 정상적인 순서와 같은 것이 있는지 궁금해하고있다. (또는 단순한 기계가이 문제를 결정 론적으로 해결하는 것은 불가능합니다.)
그래서 내가 그랬어. 아마도 대답은 비판적으로 "단순한 논리 해결사"가 무엇인지에 달려 있습니다. 그래서 나는 에 간단히을 설명하려고 시도 할 것이다.
내 프로그램은 밀접하게 프로그래밍 (제레미 기븐스 & Oege 드 무어)의 재미의 9 장에 콤비의 시스템을 기반으로합니다.
솔버의 입력은 단일 조건 수 있습니다 : 언어는 다음과 같은 구조를 가지고 있습니다. 술어에는 변수가 포함될 수 있습니다. 해석기의 출력은 0보다 크거나 솔루션입니다. 솔루션은 술어가 참이되게하는 일련의 변수 할당입니다.
변수는 표현을 유지합니다. 표현식은 정수, 변수 이름 또는 하위 표현식의 튜플입니다.
표현식 (술어가 아닌)과 동일한지를 비교하는 등호 술어가 있습니다. 모든 (바운드) 변수를 그 값으로 대체하면 두 표현식이 동일하게 만들어집니다. (특히, 모든 변수는 바운드인지 아닌지 자체와 동일합니다.)이 술어는 통합을 사용하여 해결됩니다.
AND 및 OR 연산자가 있으며, 분명히 작동합니다. NOT 연산자가 없습니다.
기본적으로 로컬 변수를 만드는 "exists"연산자가 있습니다.
술어으로 명명 된 을 정의하는 기능은 재귀 루핑을 사용 가능하게합니다. 논리 프로그래밍에 대해 "흥미로운 것들"의
하나는 명명 된 술어를 작성하면, 그것은 일반적으로 fowards 뒤로 (때로는 옆)를 작동합니다. 표준 예 : 두 목록을 연결하는 술어는 가능한 모든 쌍으로 목록을 분할하는 데 사용될 수 있습니다.
그러나 용어의 순서를 다시 정렬하지 않는 한, 때때로 술어를 거꾸로 실행하면 무한 검색이 수행됩니다. (예 : AND 또는 OR의 LHS 및 RHS를 교환하십시오.) 솔루션 세트가 실제로있는 모든 경우에서 즉각적인 종료를 보장하기 위해 술어를 실행하기위한 최상의 순서를 탐지하는 자동화 된 방법이 있는지 궁금합니다. 한정된.
제안 사항?
다른 결과. –
@ n.m. 좋은 생각. 나는 최소한의 예를 생각해 내려고 노력할 것입니다. – MathematicalOrchid
이전에 보지 못했을 경우에 대비하여 [프레스 버거 산술] (http://en.wikipedia.org/wiki/Presburger_arithmetic)도 참조하십시오. 유효성은 결정할 수 있습니다. , and, or, not, for, 및 induction을 허용합니다 (유도가 사용자가 설명하는 재귀만큼 강력하지는 않지만). –