서브섬션 격자

Subsumption lattice
그림 1: 서브섬션 격자의 비모형 하위 격자5 N

아흡수 격자는 자동화된 정리 증명과 기타 상징적인 계산 어플리케이션의 이론적 배경에 사용되는 수학 구조물이다.

정의

t라는1 용어는 t 수익률1 t에2 σ이 적용되는 대체 σ이 존재하는 경우 t라는 용어를2 소급한다고 한다.이 경우 t를1 t보다2 일반적이라 부르기도 하며 t를2 t보다1 구체적이거나 t의1 인스턴스라고 부른다.

주어진 서명에 대한 모든 (선주문) 조건의 집합은 부분 주문 관계 "...보다 더 구체적이다..."를 상쇄할 수 있다.

  • 변수 이름만 다를 경우 두 항을 동등하게 고려한다.[1]
  • 다른 어떤 용어보다 더 구체적인 것으로 간주되는 인공 최소 요소 Ω(과다 지정된 용어)을 추가한다.

이 격자는 아흡수 격자라 불린다.두 용어는 이들의 만남이 Ω과 다를 경우 불가능하다고 한다.

특성.

그림 2: f(a,x), f(x,x) 및 f(x,c) 용어가 쌍으로 사용할 수 없지만 동시에 사용할 수 없음을 보여주는 서브섬션 격자의 일부. (단순함을 위해 f 생략)

이 격자에서의 참가와 만남의 작전은 각각 반통일, 통일이라고 불린다.변수 x와 인위적 요소 Ω은 각각 격자의 상단 및 하단 요소다.각 기초 용어, 즉 변수가 없는 각 용어는 격자의 원자다.격자에는 예를 들어 x, g(x), g(x), g(x), g(g(x)), ...와 같은 무한 내림차인이 있지만 무한 상승 체인은 없다.

If f is a binary function symbol, g is a unary function symbol, and x and y denote variables, then the terms f(x,y), f(g(x),y), f(g(x),g(y)), f(x,x), and f(g(x),g(x)) form the minimal non-modular lattice N5 (see Pic. 1); its appearance prevents the subsumption lattice from being modular and hence also from being distributive.

주어진 용어로 가능하지 않은 일련의 용어들을 만날 때 닫을 필요는 없다; 그림 2는 반대 예를 보여준다.

t 용어의 모든 접지 인스턴스 집합을 Gnd(t)로 나타내며, 다음 속성은 유지된다.[2]

  • t는 Gnd(t), modulo renaming,
  • t는1 gnd(t1) ⊆ Gnd(t2)인 경우에만 t의2 한 예다.
  • 동일한 일련의 접지 인스턴스(instance)를 가진 항은 동일한 modulo 이름 변경이다.
  • t가 t와1 t의2 만남이라면 Gnd(t) = Gnd(t1) ∩ Gnd(t2)
  • t가 t와1 t의2 결합이라면 Gnd(t) ⊇ Gnd(t1) ∪ Gnd(t) ∪ Gnd(t2)이다.

선형 항의 '하위'

그림 5: 선형 용어의 분포 하위 표
그림 4: 선형 항에서 작성된3 M
그림 3: 선형5 항에서 작성된 N

변수의 다중 발생이 없는 항인 선형 항 집합은 서브섬션 격자의 하위 포셋이며, 그 자체도 격자다.이 격자도 하위 격자로 N과5 최소 비분배 격자 M을3 포함하며(그림 3과 그림 4 참조) 따라서 분배는 말할 것도 없고 모듈화되지 않는다.

만족 연산은 선형 항의 격자에서와 항상 같은 결과를 모든 항의 격자에서 산출한다.모든 용어의 결합 연산은 항상 선형 용어의 결합 인스턴스(instance)를 산출한다. 예를 들어 (접지) 용어의 f(a,a)와 f(b,b)는 모든 용어의 결합 단위와 선형 용어의 결합 단위에서 각각 f(x,x)와 f(x,y)를 갖는다.조인 연산이 일반적으로 동의하지 않기 때문에 선형 용어 격자는 모든 용어 격자의 하위 격자를 적절하게 사용하지 않는다.

두 개의 적절한[3] 선형 용어(즉, 반통일 및 통일)의 결합과 만남은 각각 그 경로 집합의 교차점과 결합에 해당한다.따라서 Ω을 포함하지 않는 선형 용어의 격자의 모든 하위 격자는 설정된 격자에 이형성이며, 따라서 분배적이다(그림 5 참조).

기원

분명히, 그 아흡수 격자는 Gordon D에 의해 처음 조사되었다. 플롯킨, 1970년.[4]

참조

  1. ^ 형식: 모든 항을 등가관계로 인수함...은 ...의 명칭 변경이다."; 예를 들어, f(x,y)라는 용어는 f(y,x)의 이름을 바꾼 것이지만 f(x,x)의 이름은 바꾼 것이 아니다.
  2. ^ Reynolds, John C. (1970). Meltzer, B.; Michie, D. (eds.). "Transformational Systems and the Algebraic Structure of Atomic Formulas" (PDF). Machine Intelligence. Edinburgh University Press. 5: 135–151.
  3. ^ 즉, Ω과 다른
  4. ^ Plotkin, Gordon D. (Jun 1970). Lattice Theoretic Properties of Subsumption. Edinburgh: Univ., Dept. of Machine Intell. and Perception.