은 Isabelle에서 두 개의 부분 함수가 같은 출력을 생성하지 않는다는 것을 보여주기위한 정의가 필요합니다.

Question

일부 Isabelle 술어를 삭제하기 위해 HOL-Z의 수학 툴킷을 사용하고 있습니다. 특히 나는 부분적인 함수 정의를 사용하여 필자가 작성한 Z 사양에서 관계의 일부를 정의하고있다. 여기서는 간단한 HOL 술어를 생성 할 수 있도록 스키마를 명세서로 변환한다. I 쓸 때 조건부 내에 다음

type_synonym  ('a,'b) lts = "('a*'b) set"  (infixr "<=>" 20) 

    prodZ  ::"['a set,'b set] => ('a <=> 'b) "  ("_ %x _" [81,80] 80) 
"a %x b"  == "a <*> b" 

rel   ::"['a set, 'b set] => ('a <=> 'b) set" ("_ <--> _" [54,53] 53) 
rel_def  : "A <--> B == Pow (A %x B)" 

partial_func ::"['a set,'b set] => ('a <=> 'b) set"  ("_ -|-> _" [54,53] 53) 
partial_func_def : "S -|-> R == 
    {f. f:(S <--> R) & (! x y1 y2. (x,y1):f & (x,y2):f --> (y1=y2))}" 

rel_appl  :: "['a<=>'b,'a] => 'b" ("_ %^ _" [90,91] 90) 
rel_appl_def : "R %^ x  == (@y. (x,y) : R)" 

HOL-Z 툴킷에서

정의 : 밸런스 Bbalance은 (Z)에서 두 부분 함수는

FORALL x. balance %^ x = Bbalance %^ x 

, 폼 ('a < =>'b) 이사벨 (Isabelle)에서는 잘 동작한다고 가정합니다.

어떻게 두 개의 부분 함수가 모든 'x'에 대해 완전히 분리되어 있다고 다른 점을 정의 할 수 있습니까? 즉, 두 개의 부분 함수 'balance'와 'Bbalance'에 같은 값을 적용하면 절대 동일한 값을 산출하지 않습니다. 뭔가 ...

FORALL x. balance %^ x \noteq Bbalance %^ x 

죄송합니다. 전문가의 조언을 통해 배웁니다. :).

Answer 1

rel_appl_def 규칙은 엡실론 기능을 사용합니다. Hilbert는 1921 년 Hamburg 강의 (1922)의 Stanford Encyclopedia of Philosophy (SEP) (*)에 따르면 공식 시스템에서 배제 된 중간의 원칙을 다루기 위해 선택 함수를 사용하는 아이디어를 처음 발표했습니다. 다음과 같이

엡실론 기능의 지배 공리 읽

(A x) --> (A (@ A)) 

을 고전적인 논리에서, 전 falso 혼성 곡의 때문에 (A x가) 실패하는 경우, (@ A) 어떤 해석을 할 수 있습니다. 즉, rel_appl_def 규칙은 도메인 dom R에없는 인수 x를 제공 할 때 어떤 값을 부여한다는 것을 의미합니다.

아마도 평등으로 사용하려는 것은 두 개의 부분 함수에서 다음 부울 함수 (^)가 될 것입니다. :

f^g = (dom f = dom g) & (!x. x : dom f --> f %^ x = g %^ x) 

9월는, 아마도 더 큰 현재 관심, 두 번째를 기록 정리 - 증명 시스템 HOL와 이사벨, 엡실론의 표현력에 엡실론 연산자를 사용하는 것입니다 때 나는 이해할 수없는 무엇 용어는 상당한 실질적인 이점을 제공합니다.

저는 실제로 옵션 유형을 사용하여 부분 기능을 훨씬 간단하게 처리하는 것을 보아 왔습니다. 따라서 부분 함수 f는 단순히 A => B 옵션 유형에 속합니다. 그러나 프로젝트에서 유형을 변경할 수없는 경우 요구 사항에 맞는 평등을 찾는 것이 더 바람직합니다. 위의 정의가 후보가 될 수 있습니다.

안녕

(*)
엡실론 미적분, 제레미 애비 게드와 리처드 자크
먼저 금 2002년 5월 3일을 발표; 난 그냥 알 2013
http://plato.stanford.edu/entries/epsilon-calculus/