어떤 종류의 유형 정의가 로컬 컨텍스트에서 유효합니까? 이자벨/순수/HOL 가능하지 입니다 매개 변수 또는 가정에 도입 종속 관계없이 - 이사벨의 <code>NEWS</code> 파일에서

Question

, 나는

명령 '형식 정의'이제 로컬 이론의 맥락에서 작동

을 발견했다. 논리적 환경은 글로벌 이론 문맥에서도 ( non-emptiness proof와 함께) 로컬 typedef에 대한 여러 해석을 포함 할 수 있습니다 ( ).

(이는 Isabelle2009-2로 거슬러 올라갑니다). 이것은 typedef 및 로컬 이론 컨텍스트에 관한 최신 뉴스입니까? 또한 "매개 변수 또는 가정에 대한 의존성을 도입하지 않은 채로"라는 제한이 실제로 의미하는 것은 무엇입니까?

typedef의 정의 집합에서 로캘 매개 변수를 사용할 수 없다는 것을 의미하면 typedef을 로컬 라이즈하지 않는 것으로 간주합니다 (허용되는 인스턴스는 로컬 컨텍스트 외부로 쉽게 이동하거나 나는 뭔가를 놓친다?).

의 (a typedef에 사용되는 설정은 로케일 매개 변수 V에 따라 다름) 라인을 따라 뭔가 할 수 그것을 (또는 그것을해야한다, 또는 어느 것) :

datatype ('a, 'b) "term" = Var 'b | Fun 'a "('a, 'b) term list" 

locale term_algebra = 
    fixes F :: "'a set" 
    and V :: "'b set" 
begin 

definition "domain α = {x : V. α x ~= Var x}" 

typedef ('a, 'b) subst = 
    "{α :: 'b => ('a, 'b) term. finite (domain α)}" 

end 

를 들어 I 현재 얻을 수있는 것 :

Locally fixed type arguments "'a", "'b" in type declaration "subst" 

Answer 1

몇 가지 더주의 사항 :

• 지역 이론 인프라 단순히 기존 정리 한 모듈 개념 (등 locale, class) 등 definition, theorem, inductive, function 등 정의 적 메커니즘 (즉,) 다양한 컨텍스트에서 균일하게 작업 할 수 있습니다. 이는 논리적 기반을 변경하지 않으므로 용어 매개 변수 (fixes) 또는 전제 (assumes)에 의존 할 수없는 사양 요소는 근본적으로 개선되지 않습니다. 그것들은 이미 더 큰 틀에 개조 된 것일 뿐이며, 이것은 이미 여분의 논리적 이익입니다.

• 정규 로컬 이론 대상은 locale이고 그 파생어는 class입니다. 이것은 위에서 스케치 한 원칙에 따라 로직 내에서 작동합니다. fixes 및 assumes의 컨텍스트를 통한 람다 리프팅. 더 많은 야망을 갖고있는 다른 대상도 상상할 수 있지만 용감하고 영웅적인 사람들이 구현해야합니다. 예를 들어, AWE 이론 해석 메커니즘을 다른 로컬 이론 목표로 마무리 한 다음 유형/consts/공리의 매개 변수화를 수행 할 수 있습니다. LCF 입증 자 내에서 허용 가능한 추론을 구현하기위한 명시적인 증명 항을 통과하는 통상적 인 비용으로 또는 LCF-ness를 포기하고 일부 oracle을 통해 수행하는 비용).

• 일반 위에 스케치 (및 지역화 codatatype 최근 HOL-BNF의 datatype 같은 그 유도체가) 약간의 실행 종속 유형 매개 변수에서 개선 될 수 있지만,이 빈약를 정당화하지 않는 일부 구현 노력을 의미로 typedef 지금 결과. 그것은 단지 같은 암시 인수 다형성 형 구조를 작성할 수 것 : 수출 후

  context fixes type 'a 
  begin 
  datatype list = Nil | Cons 'a list 
  end 
  

  당신은 평소와 같이 'a list을 얻을 것입니다.

  추가 합병증 : fixes type 'a가 존재하지 않습니다. Isabelle/Pure는 Hindley-Milner를 통해 암시 적으로 유형 매개 변수를 처리합니다.

Answer 2

한편이 질문은 Isabelle 메일 링리스트에서 답변을 받았습니다. 짧은 버전은 내가하려고했던 것이 단순히 불가능하다는 것입니다. 무엇 다음 것은 @makarius에 의해 설명입니다

이

[매개 변수 또는 가정에 종속성을 도입하지 않고는] 당신이 타입 사양의 문맥의 fixes/assumes를 참조 할 수 없음을 의미 -이 이사벨 논리적으로 불가능하다/순수/HOL. 단지 비공개 성 증거가 맥락 안에서 살아 있고, 결과 정리는 지역적이다. 문맥의 논리적 내용에 대한 증명의 실제 의존성은 실제로는 어렵다.

'typedef'는 가능한 범위 내에서 형식적으로 지역화되어있다. 로컬 리 제이션이란 일반적인 이론 인프라 및 컨텍스트와 함께 작업하는 것을 의미합니다. typedef의 경우 이것은 이름 공간, 구문, 파생 선언 등과 같은 논리적 인 것을 의미합니다.

이전에는 typedef를 문맥의 논리적 부분에 의존 할 수 없기 때문에 전혀 지역화되지 않았으며 많은 도구 구현은 오늘날까지 그로 인해 어려움을 겪고 있습니다. 내 구체적인 예로서

:

당신은 유형 subst의 매개 변수에 대해 다른 이름을 사용하여 범위의 충돌을 [...] 회피해야 할 것입니다. 그럼에도 불구하고 이는 논리적 인 관점에서 작동하지 않습니다. 용어 매개 변수 V에 대한 종속성은 HOL typedef에서 사용할 수 없습니다. 지역 이론 개념은 논리를 보강하는 마법적인 방법을 제공하지 않습니다. 이것은 단지 기존의 논리적 프레임 워크의 인프라입니다.이에