람다 큐브

이 글은 위키피디아의 품질 기준을 준수하기 위해 다시 쓰일 필요가 있을 수 있는데, 이는 기사의 주제에 대한 이해에 기초하는 기본 개념에 대해 대체로 일관성이 없고 혼란스럽고 오해의 소지가 있는 용어를 사용하기 때문이다. 넌 도울 수 있어. 토크 페이지에는 제안사항이 포함될 수 있다.(2020년 9월)

람다 큐브.각 화살표의 방향은 포함 방향이다.

수학논리와 유형이론에서 λ-큐브(또한 쓰여진 람다 큐브)는 헨크 바렌트레트가^[1] 시공의 미적분이 단순타입 λ-미적분의 일반화인 다른 차원을 조사하기 위해 도입한 틀이다.큐브의 각 차원은 용어와 유형 사이의 새로운 종류의 종속성에 해당한다.여기서 "의존성"이란 용어나 유형을 바인딩할 수 있는 용어나 유형의 용량을 말한다.λ-큐브의 각 치수는 다음과 같다.

• x축$(→[\displaystyle \rightarrow }$ }):$$ 종속 유형에 해당하는 항을 바인딩할 수 있는 유형.
• y축( $$${\displaystyle }$ ${\displaystyle \uparrow }$ ) : 다형성에 해당하는 유형을 바인딩할 수 있는 용어.
• z축( $$${\displaystyle }$ ${\displaystyle \nearrow$}): 유형을 바인딩할 수 있는 유형으로, ( () 유형 연산자에 해당된다.

이 세 가지 차원을 결합하는 다른 방법은 각각 다른 종류의 타이핑 시스템에 해당하는 큐브의 8 정점을 산출한다.λ-큐브는 순수형 체계의 개념으로 일반화할 수 있다.

시스템의 예

(λ→) 간단히 입력된 람다 미적분

λ-큐브에서 발견되는 가장 간단한 계통은 간단히 타이핑된 람다 미적분학으로, λ→라고도 한다.이 시스템에서 추상화를 구성하는 유일한 방법은 용어에 의존하는 용어를 타이핑 규칙과 함께 만드는 것이다.

${\displaystyle {\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Damma \;\lambda x.t:\sigma \to \}}}}$

(iii2) 시스템

시스템 F("2차 타이핑 람다 미적분"^[2]을 위해 22라고도 함)에는 다음과 같은 규칙으로 용어가 유형에 따라 달라질 수 있는 $\lambda {\displaystyle \mathrm{}}${\$displaystyle \Lambda }$로 작성된 다른 유형의 추상화가 있다$.$

${\displaystyle {\frac {\\bdash \;t:\sigma }{\Gamma \\\vdash \\\lambda \alpha .t:\Pi \alpha .\sigma }}}\}}\}\alpha {\text{{}}}}}}}}}}}}}}}\data.$

$\lambda {\displaystyle \mathrm{}}$ ${\displaystyle \Lambda }$로 시작하는 용어는 ML 유사 언어의 폴리모픽 함수와 유사하게 다른 기능을 얻기 위해 다른 유형에 적용할 수 있기 때문에 폴리모픽이라고 불린다$$.예를 들어, 다형성 정체성은

재미있다 x -> x 

OCaml의 종류는

'a -> 'a 

어떤 종류의 논증도 취할 수 있다는 의미'a그런 유형의 요소를 반환하십시오.이 유형은 type ${\displaystyle \alpha \alpha }$α → ${\displaystyle \alpha }$ α → α ${\displaystyle \Pi \alpha .\alpha \to \alpha }$ 타입에 해당한다$.$

(Ω) 시스템 Ω

시스템 F ${\displaystyle \underset{}{}}$ ${\displaystyle \underset{}{\_}}$ ${\$에서는 다른 유형에 의존하는 유형을 공급하기 위해 구조가$$ 도입된다.이를 유형 생성자라고 하며, "유형을 값으로 하는 함수"^[3]를 구축하는 방법을 제공한다.그러한 타입 생성자의 예로는 ${\displaystyle \mathsf{T}}$ R ${\displaystyle \mathsf{E}}$ :=${\displaystyle a}$ ${\displaystyle A}$ :${\displaystyle \ast }$ . ${\displaystyle \pi }$ B${\displaystyle }$.${\displaystyle }$(${\displaystyle A}$ ${\displaystyle \to }$ ${\displaystyle B}$→${\displaystyle }$B )${\displaystyle }$→ ${\displaystyle (B}$ ${\displaystyle \to }$ ${\displaystyle B}$)${\displaystyle }$→$$B {\$displaystyle {\mathsf {TRE}:=\lambda$ A$:*$가 있다.$\PI B.(A\to B)\to(B\to$ B$)\$to B$\}\backslash$$to B}.$ 여기서 "${\displaystyle }$:${\displaystyle }$∗ ${\displaystyle A$는 비공식적으로 "${\displaystyle }$ ${\displaystyle$ A$}$은(는 유형)"을$$ 의미한다.형식 매개 변수 $A{\displaystyle }$ ${\displaystyle$ $A}$을(를) 인수로$$ 삼아 A $유형{\displaystyle }$값 T ${\displaystyle \mathsf{R}}$ ${\displaystyle \mathsf{E}}$ {\$displaystyle$ ${\mathsf {TREE}$}s의 유형을 반환하는 함수$.$ 구체적인 프로그래밍에서 이 특성은 고려하기보다는 언어 내에서 유형 생성자를 정의하는 기능에 해당한다.원시적인 존재로 만들었지이전 유형 생성자는 대략 OCaml에 라벨이 붙은 잎이 있는 트리의 다음과 같은 정의에 해당한다.

타자를 치다 'a 나무 =   잎 의 'a   노드 의 'a 나무 * 'a 나무 

이 타입 생성자는 새로운 타입을 얻기 위해 다른 타입에 적용될 수 있다.예를 들어, 정수 나무 유형을 얻으려면:

타자를 치다 int_tree = 인트로 나무 

시스템 F ${\displaystyle \underset{}{}}$ ${\displaystyle \underset{}{\_}}$ ${\$은(는) 일반적으로 단독으로 사용되지 않지만$$ 유형 생성자의 독립적 특징을 분리하는 데 유용하다.^[4]

(λP) 람다-P

λπ라고도 하며 LF 논리 프레임워크와 밀접하게 관련되어 있는 λP 시스템에서는 이른바 종속형(dependent type)을 가지고 있다.이것들은 용어에 의존할 수 있도록 허용된 유형이다.이 제도의 중요한 도입 규칙은 다음과 같다.

${\displaystyle {\frac {\Gamma ,x:A\;\vdash \;B:*}{{\Gamma \;\vdash \;(\Pi x:A)B:*}}$

여기서 $\ast {\displaystyle }$ ${\displaystyle *}$은(는) 유효한 유형을 나타낸다$$.새로운 타입 생성자 ${\displaystyle \Pi}$은 Curry-Howard 이형성을 통해 범용 정량화에 대응하며$$, 시스템 λP는 전체적으로 커넥티브로서만 함축된 1차 로직에 대응한다.콘크리트 프로그래밍에서 이러한 의존적 유형의 예는 일정 길이의 벡터 유형이다. 즉, 길이는 그 유형에 따라 달라지는 용어다.

(FΩ) 시스템 Ω

System FΩ은 System F의 ${\displaystyle \Lambda }$ 생성자와$$ System F ${\displaystyle \underset{}{}}$ ${\$의 유형 생성자를 모두 결합하여, 시스템 FΩ은 유형에 따라 다른 유형과 유형에 따라 달라지는 항을 모두 제공한다$.$

(λC) 시공 미적분

큐브에서 inC로 표시되거나 ωPΩ으로 표시된 시공의 미적분학에서 이 네 가지는 동거를 특징으로 하여 유형과 항이 모두 유형과 항에 따라 달라질 수 있다.^{[1]: 130} 범용 $◻{\displaystyle }$ ${\displaystyle \square }$을(를) 제외한 모든 유형이 그 자체로 유형을 가진 용어이기$$ 때문에 용어와 유형 사이에 존재하는 명확한 경계는 다소 폐지된다.

형식 정의

단순하게 타이핑된 람다 미적분학을 기반으로 하는 모든 시스템의 경우, 큐브에 있는 모든 시스템은 β-축소 개념과 함께 첫 번째, 원시 용어, 그리고 그 용어를 입력할 수 있는 타이핑 규칙의 두 단계로 주어진다.

sorts $집합$은${\displaystyle }$S := {${\displaystyle ◻}$ , } ${\displaystyle \}}$ $}$ {\$displaystyle$ S$:=\{*,\square$\}}으로 $정의$되며,$$s {\$displaystyle s}$ 문자로 s를 나타낸다$.$$또한{\displaystyle }$ x${\displaystyle }$, ${\displaystyle y}$,${\displaystyle }$… ${\displaystyle x,y,\dots }$자로 대표되는 변수의$$ $V{\displaystyle }$ ${\displaystyle$ V$}$이(가) 있다$.$ 큐브 8개 시스템의 원시 항은 다음과 같은 구문으로 주어진다.

$\displaystyle A:=x\mid s\mid A~A\mid \lambda x:A:A.A\mid \Pi x:A.A}$

및 $A{\displaystyle }$→ ${\displaystyle B}$ ${\displaystyle A\to B}$ ${\displaystyle \pi }$ x${\displaystyle }$: ${\displaystyle A}$. ${\displaystyle B}$ ${\displaystyle \Pi x:A$를 나타낸다$$$.$$B{\displaystyle }$ ${\displaystyle x}$이(가) $B{\displaystyle }$ ${\displaystyle B$에서 무료로 발생하지 않는$$ 경우$$ B$}$

이 환경은 $\gamma {\displaystyle \mathrm{}}$ ${\displaystyle :=}$ ${\displaystyle \mathrm{\varnothing }}$ ${\displaystyle \mid }$ ∣${\displaystyle }$, , ${\displaystyle x}$: ${\displaystyle T}$ ${\displaystyle \Gamma :=\emptset \mid \Gamma ,x:T}$에 의해 일반적으로 제공된다.

β-축소 개념은 큐브의 모든 시스템에 공통적이다.작성 →${\displaystyle {}_{\beta }}$ ${\$ 규칙에$$ 의해 부여된다.

$${\displaystyle {\frac {}{{(\lambda x:A)B)~C\to _{\beta }B[C/x]}}}}$$

$${\displaystyle {\frac {B\to _{\beta }{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}$$

$${\displaystyle {\frac {A\to _{\beta }A}{\lambda x:A:A.B\to _{\beta }\lambda x:A'로.B}}$$

$${\displaystyle {\frac {B\to _{\beta }{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}$$

$${\displaystyle {\frac {A\to _{\beta }{\Pi x:A}B\to _{\beta }\Pi x:A'로.B}}$$

반사성, 전이성 폐쇄는${\displaystyle {}_{\beta }}$ ${\$라고 쓰여 있다$.$

큐브의 모든 시스템에도 다음과 같은 타이핑 규칙이 공통적이다.

$${\displaystyle {\frac {}{\vdash *:\squad {\text{(Axiom)}}}$$

$${\displaystyle {\frac {\\Gamma \vdash A:s\quad x{\text{}}}{\Gamma ,x:A\vdash x:에 발생하지 않음:A}\quad{\text{(시작)}}$$

$${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}\quad{\text{(웨이킹)}}}$$

$${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[a/x]}\quad {\text{(응용프로그램)}}}$$

$${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(변환)}}}$$

시스템 간의 차이는 다음 두 가지 타이핑 규칙에서 허용되는$$ 정렬 쌍$({}_{}$ ${1\mathrm{}}_{}$,${}_{}$s ${2\mathrm{}}_{}$) ${\textstyle(s_{1},s_{2})$에 있다.

$${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A:A.B:s_{2}}:}\쿼드 {\text{(제품)}}}$$

${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash b:B\quad \감마 ,x:A\vdash B:s_{2}}:{\감마 \vdash \lambda x:A.b:\Pi x:A.B}}\quad{\text{(절제)}}}$

규칙에서 허용되는$$ 시스템과 페어${}_{}{s\mathrm{}}_{}$ 1, ${s\mathrm{}}_{}$ 2${}_{}$) ${\textstyle(s_{1},s_{2})$ 간의 대응은 다음과 같다.

${\displaystyle(s_{1},s_{2})}$	${\디스플레이 스타일(*,*)}$	${\displaystyle(*,\square )}$	${\displaystyle(\square ,*)}$	$[\displaystyle(\square ,\square )}$
λ→
λP
λ2
λω
λP2
λωω
λω
λC

큐브의 각 방향은 한 쌍(모든 시스템에서 공유하는$$ 쌍$($ (,$\ast$) ${\textstyle(*,*)$ 제외)에 해당하며, 각 쌍은 다음 항과 유형 사이에 의존할 수 있는 하나의 가능성에 대응한다.

• $$($\ast$ ,$\ast$) ${\textstyle(*,*)}$은(는) 용어에 따라 항이 달라지도록 허용한다$$.
• $$($\ast$ ,$◻$) ${\textstyle(*,\square )}$을(를) 사용하면 용어에 따라 유형이 달라진다.
• $$($◻$ ,$\ast$) ${\textstyle (\square ,*)}$은(는) 용어가 유형에 따라 달라질 수 있도록 허용한다$$.
• $$($◻$ ,$◻$) ${\textstyle (\square ,\square )}$을(를) 사용하면$$ 유형에 따라 유형이 달라진다.

시스템 간 비교

λ→

얻을 수 있는 전형적인 파생은

$${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha }$$

$${\displaystyle \dash :*\vdash \da x:\data.x:\datable \to \to \to \data.}$$

일반적인 λ→의 ID(타입 $\alpha${\$textstyle$\ \$$}$$)와 매우 유사하다.빈 컨텍스트에서 수행할 수 있는 유일한 파생어는 $⊢$ $\ast$ :$⊢$ : ◻ ${\textstyle \vdash *:\square }$이기 때문에 사용된 모든 유형은 컨텍스트에 나타나야 한다는 점에 유의하십시오$.$

계산력이 상당히 약해 확장된 다항식(조건부 연산자와 함께 하는 폴리노멀)에 해당한다.^[5]

λ2

λ2에서는 그러한 용어는 다음과 같이 얻을 수 있다.

$${\displaystyle \vdash(\data \cHB :*)\httda x:\bot .x\boat \properties )\Pi \베타 :*.\봇 \to \베타 }$$

$\perp \mathrm{}$ =$\alpha$ :$\ast$ .$\alpha$ ${\textstyle \bot =\Pi \alpha :*$와 함께.$\alpha$ $\}.$ Curry-Howard 이소모르피즘을 통해 $via\mathrm{}$ ${\textstyle \Pi}$을 보편적 정량화로 읽으면 이는 폭발 원리의 증거로 볼 수 있다.일반적으로 λ2는$\mathrm{}$including {\$textstyle \bot$ $\}$과 같은 귀납적 유형을 가질 가능성을 추가하며, 이는 자신을 포함한 모든 유형에 대해 수량화하는 용어다.

λP

λP에서 용어에 따라 유형을 갖는 능력은 논리 술어를 표현할 수 있다는 것을 의미한다.예를 들어, 다음이 파생 가능하다.

$${\displaystyle \alpha :*,a_{0}:\alpha,p:\alpha \to *,q:*\vdash \lambda z:(\Pi x:\alpha .px\to q)\lambda y:(\Pi x:\alpha .px).(za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to(\Pi x:\alpha .px)\to q}$$

Curry-Howard 이형성을 통해 (${\displaystyle \mathrm{\forall }}$ ${\displaystyle x}$: A${\displaystyle }$, ${\displaystyle P}$ x${\displaystyle }$→ Q${\displaystyle }$)${\displaystyle }$→ (${\displaystyle \mathrm{}}$( ${\displaystyle x}$: A${\displaystyle }$, ${\displaystyle P}$ ${\displaystyle x}$)${\displaystyle }$→ ${\displaystyle Q}$ ${\displaystyle (\forall x:A,$$Px\to Q)\to (\all x:A)$$Px)\to$ Q$\}$ .

변환 규칙은 유형 내 용어에 대한 계산을 수행할 수 있기 때문에 종속 유형을 처리할 때 매우 필요하다.For instance, if you have ${\displaystyle \Gamma \vdash A:P((\lambda x.x)y)}$ and ${\displaystyle \Gamma \vdash B:\Pi x:P(y).$$C{\displaystyle \mathrm{}}$$}$,${\displaystyle }$A : ${\displaystyle P}$(${\displaystyle }$y${\displaystyle }$) ${\displaystyle \Gamma \vdash$A$:P(y)}$을(를) 얻으려면 변환 규칙을 적용해야 need$$${\displaystyle }B{\displaystyle \mathrm{}}$ ${\displaystyle A}$: ${\displaystyle C}$ ${\displaysty \Gamma \vdash BA:$$C}$.

λω

Ω으로, 다음 연산자

$$\displaystyle AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma }$$

정의 가능, 즉 $⊢{\displaystyle }$ ${\displaystyle A}$ ${\displaystyle N}$ ${\displaystyle D}$ :${\displaystyle \ast }$→${\displaystyle }$∗ →${\displaystyle \ast }$ ${\displaystyle \vdash AND:*\to$ 파생어

$$\displaystyle \alpha :*,\beta :\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*}$$

λ2에서 이미 얻을 수 있지만, 다형성 $A$ $N$ $D$ ${\textstyle AND}$은(는) 규칙$){\textstyle(\square ,*)$도 있는$$ 경우에만 정의할 수 있다$$.

컴퓨팅의 관점에서 λω는 극히 강하며, 언어 프로그래밍의 기초로서 여겨져 왔다.^[8]

λC

시공의 미적분은 predP의 술어 표현력과 λω의 연산력을 모두 가지고 있기 때문에 cC를 ωPΩ이라고도 부르기 ^{[1]: 130} 때문에 논리적인 측면과 계산적인 측면 모두에서 매우 강력하다.

다른 시스템과의 관계

Automath 시스템은 논리적인 관점에서 λ2와 유사하다.ML과 같은 언어들은 타이핑의 관점에서 볼 때, 제한된 종류의 다형체를 인정하기 때문에 λ→λ2의 어딘가에 놓여 있는데, 그것은 혼전 정상적인 형태의 유형이다.그러나, 일부 재귀 연산자를 특징으로 하기 때문에, 이들의 연산력은 λ2보다 크다.^[7]Coq 시스템은 단 하나의 전형적이지 않은${{\textstyle \square$}$$, 그리고 유도 유형을 구성할 수 있는 능력이 아니라 우주의 선형 계층 구조를 가진 λC의 확장에 기반을 두고 있다.

순수형 시스템은 임의의 종류, 공리, 제품 및 추상화 규칙 집합을 가진 큐브의 일반화라고 볼 수 있다.Conversely, the systems of the lambda cube can be expressed as pure type systems with two sorts ${\displaystyle \{*,\square \}}$, the only axiom ${\textstyle \{*,\square \}}$, and a set of rules ${\textstyle R}$ such that ${\displaystyle \{(\ast ,\ast ,\ast )\}\subseteq R\subseteq \{(\ast ,\ast ,\ast ),(\ast ,◻,◻),(◻,\ast ,\ast ),(◻,◻,}$${\displaystyle ◻}$)$}$ {\$displaystyle \{(*,*,*)\}\subseteq$R\$subseteq \{(*,*,*,*),$ (\$square,*), (\$square,*), $(\square,\square$ $)\backslash \}\}.$^[1]

커리-하워드 이소모르피즘을 통해 람다 큐브에 있는 시스템들과 논리 시스템들 사이에 일대일 대응,^[1] 즉 다음과 같은 것이 있다.

모든 로직은 타당하지만$($즉, 유일한$$ 커넥티브는$$→ ${\textstyle \to }$ 및 $\forall \mathrm{}$ ${\textstyle$ $\wedge },$ $\neg {\displaystyle \mathrm{}}$ ${\$$displaystyle$ \wedge } 또는$$ ¬ {\$displaysty \neg}$ 등)와 같은 다른 커넥티브는 2차 이상의 로직렬 로직으로 정의할$$ 수 있다.$$약한 고차 로직에서는 고차 술어에 대한 변수가 있지만, 고차 술어에 대한 계량화는 수행할 수 없다.

공통 속성

큐브의 모든 시스템이 즐기십시오.

• the Church-Rosser property: if ${\displaystyle M\to _{\beta }N}$ and ${\displaystyle M\to _{\beta }N'}$ then there exists ${\displaystyle N''}$ such that ${\displaystyle N\to _{\beta }^{*}N''}$ and ${\displaystyle N'\to _{\beta }^{*}N''}$;
• 환자 감소 속성: ${\displaystyle \gamma }$ ${\displaystyle ⊢}$ ${\displaystyle M}$: T ${\displaystyle \Gamma \vdash M:$$T}$ 및$$ $M{\displaystyle {}_{}}$→ ${\displaystyle {\beta }_{}}$ ${\displaystyle {}_{}{}^{}}$ ${\displaystyle {\prime }^{}}$ ${\$ 다음에$$ $\gamma {\displaystyle \mathrm{}}$ ${\displaystyle ⊢}$ ${\displaystyle {}^{}}$ ${\displaystyle {\prime }^{}}$: ${\displaystyle T}$ ${\displaystyle \Gamma$ \$vdash M':T$
• 유형의 고유성: ${\displaystyle \gamma }$ ${\displaystyle ⊢}$ ${\displaystyle A}$: B ${\displaystyle \Gamma \vdash A:B}$ 및$$ $\gamma {\displaystyle \mathrm{}}$ ${\displaystyle ⊢}$ ${\displaystyle A}$: ${\displaystyle {}^{}}$ ${\displaystyle {\prime }^{}}$ ${\$$B'}$ 다음에$$ $B{\displaystyle }$ =${\displaystyle {}_{\beta }}$ ${\displaystyle {}_{}{}^{}}$′ ${\$

이 모든 것들은 일반 순수형 시스템에서 증명될 수 있다.^[9]

큐브 시스템에서 잘 타이핑된 용어는 모든 순수 유형 시스템에 공통적인 것은 아니지만 강하게 정상화되고 있다.^[1]큐브에 튜링이 완료된 시스템이 없음.^[7]

서브타이핑

그러나 서브타이핑과 다형성을 결합한 고차 경계 정량화로 알려진 ${\$과 같은 시스템이 실질적인 관심사가 되고 있으며, 더 나아가 경계형 연산자로 일반화될 수 있음에도 불구하고 서브타이핑은 큐브에 나타나지 않는다. ${\$omega $}}}}$에 대한 추가 확장은 순전히 기능적인 객체의 정의를 가능하게 한다. 이러한 시스템은 람다 큐브 페이퍼가 간행된 후 일반적으로 개발되었다.^[10]

큐브 아이디어는 수학자 헨크 바렌드렛(1991) 때문이다.순수형 시스템의 프레임워크는 큐브의 모든 모서리와 다른 많은 시스템들이 이 일반적인 프레임워크의 인스턴스로 표현될 수 있다는 의미에서 람다 큐브를 일반화한다.^[11]이 틀은 람다 큐브를 2년 앞서게 한다.1991년 논문에서 바렌트레트는 이 틀에서 큐브의 모서리를 규정하기도 한다.

참고 항목

• Olivier Ridoux는 그의 Habilitation a diriger lesherches에서 람다 큐브의 컷아웃 템플릿과 8개의 꼭지점이 면으로 대체되는 옥타헤드론으로서 큐브를 이중으로 표현하고 12개의 가장자리가 면으로 대체되는 도데케드론으로서의 이중 표현을 제공한다.^[12]
• 호모토피형 이론

메모들

추가 읽기

• Peyton Jones, Simon; Meijer, Erik (1997). "Henk: A Typed Intermediate Language" (PDF). Henk is based directly on the lambda cube, an expressive family of typed lambda calculi.

외부 링크

• 로저 비숍 존스(Roger Bishop Jones)의 순수형 시스템 맥락에서 바렌드레트의 람다 큐브(Lambda Cube)