유도 재귀

수학 논리학의 한 분야인 직관적 유형 이론(ITT)에서, 유도 재귀는 유형과 함수를 동시에 선언하는 특성이다.그것은 유도형보다 우주와 같은 더 큰 형태의 창조를 가능하게 한다.생성된 유형은 ITT 내에서 여전히 문제가 됩니다.

귀납적 정의는 유형의 요소를 생성하기 위한 규칙에 의해 주어진다.그런 다음 유형의 요소가 생성되는 방식에 따라 유도함으로써 해당 유형의 함수를 정의할 수 있습니다.유도 재귀는 유형과 함수를 동시에 정의할 수 있기 때문에 이 상황을 일반화합니다.유형의 요소를 생성하는 규칙은 ^[1]함수를 참조할 수 있기 때문입니다.

유도 재귀는 다양한 우주 구조를 포함한 큰 유형을 정의하는 데 사용할 수 있습니다.그것은 유형 이론의 입증 이론 강도를 상당히 증가시킨다.그럼에도 불구하고, 귀납적-재귀적 정의는 여전히 서술적인 것으로 간주됩니다.

배경

유도-재귀는 마틴-뢰프의 직관적 유형 이론의 규칙에 대한 조사로부터 나왔다.활자 이론에는 많은 "활자 형성자"와 각각에 대한 4가지 규칙이 있습니다.마틴-뢰프는 각 유형의 규칙이 유형 이론의 특성을 보존하는 패턴을 따른다는 것을 암시했다.연구자들은 그 패턴에 대한 가장 일반적인 설명을 찾기 시작했는데, 그 이유는 그것이 활자 이론을 확장하기 위해 어떤 종류의 활자 형성기가 추가될 수 있는지를 말해주기 때문이다.

"우주"형 전자가 가장 흥미로웠다. 왜냐하면 규칙이 "아 라 타르스키"로 작성되었을 때, 그들은 "우주형"과 그에 대해 작동하는 함수를 동시에 정의했기 때문이다.결과적으로 다이버는 유도-재귀로 이어집니다.

Dybjer의 초기 논문들은 유도-재귀가 규칙에 대한 "계획"이라고 불렀다.그것은 활자 이론에 어떤 활자 형성자를 추가할 수 있는지를 명시했다.나중에, 그와 세처는 새로운 유도-재귀 정의를 유형 ^[2]이론 안에서 만들 수 있는 규칙과 함께 새로운 유형 전자를 썼다.이것은 하프 프루프 어시스턴트(Alf의 변형)에 추가되었습니다.

아이디어

유도-재귀 유형을 다루기에 앞서, 간단한 사례는 유도 유형입니다.유도형 생성자는 자기 참조형일 수 있지만 제한적입니다.생성자의 매개 변수는 "양수"여야 합니다.

정의되고 있는 타입을 참조하지 않는다.
정의되고 있는 타입이 바로 그것입니다.
정의 중인 유형을 반환하는 함수입니다.

유도 유형의 경우 매개 변수의 유형은 이전 매개 변수에 따라 달라질 수 있지만 정의되는 유형의 매개 변수를 참조할 수는 없습니다.유도-재귀 유형은 더 나아가 파라미터 유형은 정의되는 유형을 사용하는 이전 파라미터를 참조할 수 있습니다.다음은 "반양성"이어야 합니다.

정의 중인 함수에 이전 매개변수가 랩되어 있는 경우 해당 매개변수에 따라 함수가 됩니다.

따라서 D{\ $displaystyle$ D $}$ 가 $D$ 정의되는 $f$ 이고f {\ $displaystyle$ f $}$ 가 $f$ 정의되는 함수인 $경우$ 다음 파라미터 선언은 양수입니다.

$a:A$
$d:D$
$g:A\to 타입$
$h:A\to D$
${\displaystyle i:A에서 B로$
$j:g\ a$ : $j:g\ a$ \ $display style$ $j:g\ a$ j : $g$ \ $a$ $j:g\ a$ （ $D$ $))))))))))))))$ $D$ 은 없습니다)

이것은 반양성입니다.

$k:(f\ d)\to D$ : $k:(f\ d)\to D$ ( $k:(f\ d)\to D$ ) $k:(f\ d)\to D$ {\ $displaystyle k:(f\d$ )\ $to$ D} ( $D$ 의 $D$ $파라미터$ d {\ $displaystyle$ d $}$ 에 $d$ 의존하지만f {\ $displaystyle$ f $}$ 에 대한 호출을 통해서만)

이것들은 긍정적이지도 않고 반긍정적이지도 않다.

$k:D\to A$ $D\to$ A $($ $\displaystyle$ D는 $D$ 함수의 파라미터입니다).
$l:(A\to D)\to A$ : $l:(A\to D)\to A$ ( $l:(A\to D)\to A$ $l:(A\to D)\to A$ ) $l:(A\to D)\to A$ $l:(A\to D)\to A$ {\ $displaystyle$ l $:(A\to$ D $)\to$ A $l:(A\to D)\to A$ } (파라미터는 D{\ $displaystyle$ D $D$ 를 반환하는 함수를 사용하지만 A{\ $displaystyle$ A $}$ 자체를 $A$ $A$ 함)
$m:z\ d$ : $m:z\ d$ d \ $display style$ m : $z$ \ $d$ （ $m:z\ d$ $d$ ）（ $d$ )) D $）$ 。 $단$ , f $\$ $display style$ f)))))) ))))))))))))))))D\ $d$ 에 $d$ $d$ 합니다.) $f$

우주의 예

단순한 일반적인 예로는 우주 타르스키 타입의 전자가 있습니다. $타입$ U $(디스플레이 스타일$ U $)$ 와 $U$ $함수$ T $(디스플레이 스타일$ T $T$ 를 $U$ 만듭니다.타입 이론의 모든 타입에는 U $($ $디스플레이 스타일 U!)$ $U$ 가 $U$ $있습니다$ . $T$ {\ $displaystyle$ T $}$ 함수는 $T$ U{\ $displaystyle$ U $}$ $U$ 를 $U$ 관련 유형에 매핑합니다.

$유형$ U {\ $displaystyle$ U $}$ 에는 $U$ 유형 이론의 각 유형에 대한 생성자(또는 도입 규칙)가 있습니다.종속 기능에 대한 것은 다음과 같습니다.

$컨스트럭터_{\Pi }(u:U)(u'):T(u)\to U:U$

즉, 파라미터의 유형에 매핑되는 $유형$ U(\ $displaystyle$ U $)$ 의 $U$ 요소u(\ $displaystyle$ u)와 $u$ $x:T(u)$ 값 x $(\displaystyle$ x $:T(u$ 에 대해 $($ x $u'(x)$ 가 $반환$ 되는 함수 u(\ $displaystyle u)$ 가 $u'$ $u'(x)$ $u'$ 합니다 $.$ 파라미터 $값$ x $(\displaystyle$ x $)($ 최종 $:$ $\displaystyle:$ $U}$ 는 $:U$ 컨스트럭터의 결과가 $U형$ 요소(\ $displaystyle$ U $)$ 라고 합니다.

축소(또는 계산 규칙)에는 다음과 같이 기재되어 있습니다.

$T(constructor_{\Pi }(u,u'))$ becomes ${\displaystyle \prod _{x:$ $T(u)}T(u'(x$

축소 후에는 $\displaystyle$ T 기능이 입력의 $T$ 작은 부분에서 작동합니다.T{\ $displaystyle$ T $}$ 가 $T$ 컨스트럭터에 적용되었을 때 이 $T$ 가유지되면 T {\ $displaystyle$ T $}$ 는 $T$ 항상 종료됩니다.상세하게 설명하지 않고, 유도 재귀는 함수 호출이 항상 종료되도록 이론에 추가할 수 있는 정의(또는 규칙)의 종류를 기술합니다.

사용.

유도-재귀는 Agda 및 Idris에서 ^[3]구현됩니다.

「」를 참조해 주세요.

유도 유도 - 유형과 유형군을 동시에 정의하는 추가 작업

레퍼런스

^ Dybjer, Peter (June 2000). "A general formulation of simultaneous inductive-recursive definitions in type theory" (PDF). Journal of Symbolic Logic. 65 (2): 525–549. CiteSeerX 10.1.1.6.4575. doi:10.2307/2586554. JSTOR 2586554.
^ Dybjer, Peter (1999). A finite axiomatization of inductive-recursive definitions. Lecture Notes in Computer Science. Vol. 1581. pp. 129–146. CiteSeerX 10.1.1.219.2442. doi:10.1007/3-540-48959-2_11. ISBN 978-3-540-65763-7.
^ Bove, Ana; Dybjer, Peter; Norell, Ulf (2009). Berghofer, Stefan; Nipkow, Tobias; Urban, Christian; Wenzel, Makarius (eds.). "A Brief Overview of Agda – A Functional Language with Dependent Types". Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 73–78. doi:10.1007/978-3-642-03359-9_6. ISBN 978-3-642-03359-9.

외부 링크

[Dybjer-1] Dybjer, Peter (June 2000). "A general formulation of simultaneous inductive-recursive definitions in type theory" (PDF). Journal of Symbolic Logic. 65 (2): 525–549. CiteSeerX 10.1.1.6.4575. doi:10.2307/2586554. JSTOR 2586554.

[DybjerSetzer-2] Dybjer, Peter (1999). A finite axiomatization of inductive-recursive definitions. Lecture Notes in Computer Science. Vol. 1581. pp. 129–146. CiteSeerX 10.1.1.219.2442. doi:10.1007/3-540-48959-2_11. ISBN 978-3-540-65763-7.

[3] Bove, Ana; Dybjer, Peter; Norell, Ulf (2009). Berghofer, Stefan; Nipkow, Tobias; Urban, Christian; Wenzel, Makarius (eds.). "A Brief Overview of Agda – A Functional Language with Dependent Types". Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 73–78. doi:10.1007/978-3-642-03359-9_6. ISBN 978-3-642-03359-9.

[1]

[2]

[3]

Search

유도 재귀

네임스페이스

더

목차

배경

아이디어

우주의 예

사용.

「」를 참조해 주세요.

레퍼런스

외부 링크

Search

유도 재귀

배경

아이디어

우주의 예

사용.

「 」를 참조해 주세요.

레퍼런스

외부 링크

「」를 참조해 주세요.