해석되지 않은 함수

Uninterpreted function

수학 논리학에서 해석되지[1] 않은 함수 또는 함수[2] 기호는 이름과 n-ary 형식 외에는 다른 속성이 없는 함수입니다.함수 기호는 상수 및 변수와 함께 항을 형성하는 데 사용됩니다.

해석되지 않은 함수의 이론은 자유 이론이라고도 불리는데, 왜냐하면 자유 이론이 자유롭게 생성되기 때문에 자유 물체 또는 빈 이론이 빈 문장 집합을 가지고 있기 때문입니다(초기 대수에 비유).방정식의 집합이 비어있지 않은 이론은 평등 이론으로 알려져 있다.자유이론의 만족도 문제는 통사적 통일에 의해 해결된다; 후자의 알고리즘은 프롤로그와 같은 다양한 컴퓨터 언어에 대해 통역자에 의해 사용된다.통사적 통일은 또한 특정 다른 동등 이론의 충족 가능성 문제에 대한 알고리즘에서도 사용됩니다. "전자 통일 및 좁히기"를 참조하십시오.

예

SMT-LIB에 대한 해석되지 않은 함수의 예로서 이 입력이 SMT 솔버에 제공되는 경우:

(declare-fun f (Int) Int)(예: (= (f 10) 1))

SMT 솔버는 "This input is perfectable"을 반환합니다.그런 일이 생기는 건f해석되지 않은 함수(즉, 에 대해 알려진 모든 것)입니다.f시그니처)이기 때문에f(10) = 1다만, 이하의 입력을 적용하면,

(declare-fun f (Int) Int)(예: (= (f 10) 1))(예: (= (f 10) 42)

SMT 솔버는 "이 입력은 만족스럽지 않습니다"를 반환합니다.그런 일이 생기는 건f는 함수이므로 같은 입력에 대해 다른 값을 반환할 수 없습니다.

논의

자유이론의 결정문제는 많은 이론들이 그것에 의해 [3]축소될 수 있기 때문에 특히 중요하다.

자유이론은 합동폐쇄를 [clarification needed]형성하기 위해 공통 하위식을 검색함으로써 풀 수 있다.해결사에는 만족도 모듈로 이론 해결사가 포함됩니다.

「 」를 참조해 주세요.

메모들

레퍼런스

  1. ^ Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4.
  2. ^ Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.
  3. ^ de Moura, Leonardo; Bjørner, Nikolaj (2009). Formal methods : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers (PDF). Berlin: Springer. ISBN 978-3-642-10452-7.
Stub icon

이 정식 메서드 관련 기사는 stub입니다.위키피디아를 확장함으로써 위키피디아를 도울 수 있습니다.