에르브랑 구조

1차 논리에서 에르브랑 구조 $S$ (영어: Herbrand structure)는 어휘 $\sigma$ (때로는 서명이라고도 함)에 대한 구조로, $\sigma$ 의 통사적 속성에 의해서만 정의된다. 아이디어는 항의 기호 문자열을 값으로 취하는 것이다. 예를 들어, 상수 기호 $c$ 의 표기는 단순히 " $c$ " (기호)이다. 이는 자크 에르브랑의 이름을 따서 명명되었다.

에르브랑 구조는 논리형 프로그래밍의 기초에서 중요한 역할을 한다.^[1]

에르브랑 해석 영역

정의

에르브랑 해석 영역은 에르브랑 구조에서 해석 영역 역할을 한다.

1차 언어 $L^{\sigma }$ $L^{\sigma }$ 의 에르브랑 해석 영역은 $L^{\sigma }$ $L^{\sigma }$ 의 모든 바닥항들의 집합이다. 언어에 상수가 없으면, 임의의 새로운 상수를 추가하여 언어를 확장한다.
- $\sigma$ 가 가산이고 0보다 큰 항수를 가진 함수 기호가 존재하면, 에르브랑 해석 영역은 가산 무한하다.
- 1차 언어의 맥락에서 우리는 단순히 어휘 $\sigma$ 의 에르브랑 해석 영역이라고도 말한다.
스콜렘 표준형의 닫힌 공식 $F$ $F$ 의 에르브랑 해석 영역은 $F$ $F$ 의 함수 기호와 상수를 사용하여 구성할 수 있는 모든 변수 없는 항들의 집합이다. $F$ $F$ 에 상수가 없으면, 임의의 새로운 상수를 추가하여 $F$ $F$ 를 확장한다.
- 이 두 번째 정의는 계산적 분해 증명의 맥락에서 중요하다.

예시

어휘가 다음과 같은 1차 언어 $L^{\sigma }$ 가 있다고 하자.

상수 기호: $c$
함수 기호: $f(\cdot ),\,g(\cdot )$

그러면 $L^{\sigma }$ (또는 $\sigma$ )의 에르브랑 해석 영역 $H$ 는 다음과 같다.

$H=\{c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),\dots \}$

관계 기호는 관계만 포함하는 공식이 해석 영역의 원소에 해당하지 않으므로 에르브랑 해석 영역과는 관련이 없다.^[2]

에르브랑 구조

에르브랑 구조는 에르브랑 해석 영역 위에 항들을 해석한다.

정의

어휘 $\sigma$ 와 해석 영역 $U$ 를 가진 구조 $S$ 가 있다고 하자. $W$ 는 $\sigma$ 에 대한 모든 항들의 집합이고, $W_{0}$ 는 모든 변수 없는 항들의 부분집합이라고 하자. $S$ 가 에르브랑 구조인 것은 다음을 만족할 때이다.

$U=W_{0}$
모든 $n$ 항 함수 기호 $f\in \sigma$ 와 $t_{1},\dots ,t_{n}\in W_{0}$ 에 대해 $f^{S}(t_{1},\dots ,t_{n})=f(t_{1},\dots ,t_{n})$
$\sigma$ 의 모든 상수 $c$ 에 대해 $c^{S}=c$