패턴 매칭 (예 : Prolog, ML 패밀리 언어 및 다양한 전문가 시스템 쉘에서 발견됨)은 일반적으로 엄격한 순서로 데이터 요소와 쿼리를 일치시켜 작동합니다.연관 및 교환 연산자와의 패턴 일치
그러나 자동 정리 정리와 같은 도메인에서는 일부 연산자가 연관성 있고 교환 가능하다는 점을 고려해야한다는 요구 사항이 있습니다. 우리는이 일치하지 않는 표면 구문으로가는 데이터
A or B or C
C or $X
이 있다고 가정하지만, or이 연관 및 교환 법칙이 성립하기 때문에 논리적으로는 A or B에 바인딩 $X와 일치해야합니다.
어떤 언어로든 이런 종류의 일을하는 기존 시스템이 있습니까?
연관 - 교환 패턴 매칭은 1981 and earlier부터 있었고, 아직도 화제 인 today입니다.
이 아이디어를 구현하고 유용한 시스템이 많이 있습니다. associtivity 또는 commutativity를 사용하여 패턴 일치를 만들 때 복잡한 패턴 일치를 작성하는 것을 피할 수 있음을 의미합니다. 예, 비쌀 수 있습니다. pattern matcher가 자동으로 이렇게하는 것이 더 낫습니다.
rewrite system for algebra and simple calculus의 예는 프로그램 변환 시스템을 사용하여 구현할 수 있습니다. 이 예에서 처리 할 기호 언어는 문법 규칙에 의해 정의되고 A-C 속성이있는 규칙이 표시됩니다. 기호 언어를 파싱하여 생성 된 트리에 다시 쓰기가 자동으로 확장되어 일치시킵니다.
나는 이런 일이 발생하지 않았으며 방금 좀 더 자세히 살펴 보았습니다.
기본적으로이 기능을 구현하지 않는 이유가 있습니다. 패턴 일치 전에 입력의 모든 조합을 생성해야하며 그렇지 않으면 일치 항목의 전체 제품 간 가치를 생성해야합니다.
일반적인 구현 방법은 두 패턴 (이진 경우)을 쓰는 것, 즉 C or $X과 $X or C의 패턴을 모두 작성하는 것입니다.
데이터의 기본 구성 (일반적으로 튜플 임)에 따라이 패턴 일치는 튜플 요소의 순서를 재정렬하는 것을 포함합니다. 특히 터프한 환경에서 그렇습니다. 그 대신에 목록이라면, 당신은 심지어 더 흔들리는 땅에 있습니다. 덧붙여
, 난 당신이 근본적으로 원하는 작업이 세트에 연결되지 않은 노조 패턴이라고 생각 예 :
foo (Or ({C} disjointUnion {X})) = ...
모든 세부 사항 세트를 다루는 내가 본 유일한 프로그래밍 환경이 될 것이다 이자벨/HOL , 그리고 나는 여전히 당신이 그들과 패턴 매치를 만들 수 있는지 확신하지 못한다.
편집 : 그것은 당신이 일관되게 사용된다는 것을 증명해야 다음을 제외하고, 복잡한 비 생성자 패턴을 정의 할 것이다 (오히려 fun 이상) 이사벨의 function 기능과 같은, 당신은 더 이상 코드 생성기를 사용할 수 없습니다.
편집 2 : 쿼리와 일치하는 것이 허용되었다 $X 형태 B | C | $X,의 동안
내 용어, 양식 A | B | C | D의했다 : 나는 n 교환 법칙, 결합 및 전이 사업자를 통해 비슷한 기능을 구현하는 방법이이었다 0 개 이상. 나는 lexographic 순서를 사용하여 이들을 미리 정렬 했으므로 변수는 항상 마지막 위치에서 발생했습니다.
먼저 모든 쌍방향 일치를 구성하고 지금은 변수를 무시하고 규칙에 따라 일치하는 것을 기록합니다.이은으로 된 그래프로 처리하는 경우
{ (B,B), (C,C) }
, 당신은 본질적으로 perfect marriage 문제를하고 있습니다. 이를 찾는 빠른 알고리즘이 있습니다.
다음 (예, A 및 D에서) 관계의 왼쪽에 나타나지 않는 모든 것을 수집하고 변수 $X로 물건, 당신의 이상형, 당신이 하나를 찾을 가정 완전한. 분명히 여기서 모든 단계에서 실패 할 수 있지만, RHS에 변수가 없거나 LHS에 일치하는 (전혀 일치하지 않는) 생성자가있는 경우 대부분 발생합니다.
조금 혼란 스럽다면 죄송합니다. 이 코드를 작성한 지 오래되었지만이 코드가 도움이되기를 바랍니다.
레코드의 경우이 은 일 수 있습니다. 모든 경우에 좋은 방법은 아닙니다. 나는 서브 테임 (즉, 단순한 평등이 아니라)에 '매치'라는 매우 복잡한 개념을 가지고 있었기 때문에 세트 나 아무것도 제작하지 않았을 것입니다. 어쩌면 그것은 당신의 경우에 작동 할 것이고 분리 된 노동 조합을 직접 계산할 수 있습니다.
필자가 생각하기에이 방식을 구현하는 방법은 튜플 기반 표현을 집합 표현으로 변환하여이 유형의 쿼리를 합리적으로 효율적으로 수행 할 수 있도록하는 것입니다. 나는 누군가가 이미이 특정한 바퀴를 처음으로 발명했는지 알기 위해 점검할만한 가치가 있다고 생각했다. – rwallace
나는 bigraphs를 위해 모델 검사기에서 비슷한 것을 구현했다. bigraphs에 대한 병렬 구성은 교환 적 (commutative)이므로이 기능을 정확히 구현해야했습니다. 구현하는 것이 대부분 끔찍한 일이었습니다.이 코드는 사용 가능하지만 다른 bigraph와 일치하는 코드가 매우 유용하고 재사용 가능성이 적기 때문에 도움이되지 않을 것으로 생각됩니다. 내가 그것을 구현하는 방법을 스케치 내 대답을 편집합니다. – Gian
감사! Upvoted; 나는 downvote가 누구에게서 왔는지 모른다. – rwallace
maude 용어 다시 작성기는 연관 및 교환 가능 패턴 일치를 구현합니다.
더 구체적인 링크를 제공 할 수 있습니까? 코드 예제가 있을까요? –
은 내가 ML 패턴 매칭 대 프롤로그 패턴 매칭의 당신의 융합에 동의 모르겠어요. ML 패턴 일치는 순전히 통사론이며, Prolog에서는 이것이 사실이라고 생각하지 않습니다. – Gian
나는 그것들이 똑같은 것을 말하는 것이 아니라, 그들이 엄격한 순서로 요소들의 비교를 공통적으로 갖는다는 것을 말하고있다. – rwallace
나는 오터 (Otter)와 같은 소프트웨어를 증명하는 헌신적 인 이론은 이미 논리적 공식을 일반 형식으로 배치하고 절을 작성 및 검증을위한 O (n log n) 시간의 비용을 요하는 집합 데이터 구조로 취급한다고 가정합니다. 사실, 나는 그들이 associativity 및 commutativity 같은 속성에 대한 작업에 대한 최적화를 미리 프로그래밍했다고 가정합니다. –