입력된 람다 미적분

이 글은 검증을 위해 인용구가 추가로 필요하다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "타입 람다 미적분" – 뉴스 · 신문 · 책 · 학자 · JSTOR (2015년 3월) (이 템플릿 메시지를 제거하는 방법과 시기 학습)

입력된 람다 미적분은 익명 함수 추상화를 나타내기 위해 람다-심볼( ${\displaystyle }$ ${\displaystyle \lambda }$)을 사용하는 형식주의 형식이다.이러한 맥락에서, 형식은 보통 람다 용어에 할당되는 통사적 성격의 개체로, 형식의 정확한 성질은 고려된 미적분학에 따라 달라진다(아래 종류 참조).어떤 관점에서는 타이핑된 람다 미적분을 정교하게 다듬은 것으로 볼 수 있지만, 또 다른 관점에서는 더 근본적인 이론과 타이핑되지 않은 람다 미적분 역시 한 가지 유형만을 가진 특수한 경우라고 볼 수 있다.

타이핑된 람다 칼쿨리는 기초 프로그래밍 언어로서 ML, Haskell과 같은 타이핑된 기능 프로그래밍 언어와 보다 간접적으로 타이핑된 명령 프로그래밍 언어의 기반이다.입력된 람다 칼쿨리는 프로그래밍 언어를 위한 형식 시스템의 설계에 중요한 역할을 한다. 여기서, 타이핑은 일반적으로 프로그램의 바람직한 속성을 포착한다(예: 프로그램은 메모리 액세스 위반을 유발하지 않는다).

활자 람다 미적분은 Curry-Howard 이형태를 통한 수학 논리학 및 증명 이론과 밀접하게 관련되어 있으며, 그것들은 범주 등급의 내부 언어로 간주될 수 있다. 예: 단순 활자 람다 미적분은 CCC(Cartesian Closed Category)의 언어다.

활자형 람다 칼쿨리의 종류

다양한 형태의 람다 칼쿨리가 연구되어 왔다.간단히 타이핑된 람다 미적분학에는 화살표${\displaystyle }$→ ${\displaystyle \to$ 기본 유형 및 함수 유형 ${\displaystyle \to }$ → → → ${\displaystyle \tau }${\$displaystyle \sigma \to \to$ $\},$ 시스템 T는 단순히 타이핑된 람다 미적분학을 자연적인 숫자와 높은 순서로 확장한다. 이 시스템에서는 모두 재미있다.Peano 산술에서 확실히 재귀적인 CTion은 정의 가능하다.시스템 F는 모든 유형에 대해 보편적 정량화를 사용함으로써 다형성을 허용한다; 논리적인 관점에서 그것은 2차 논리적으로 총체적일 수 있는 모든 기능을 설명할 수 있다.종속형인 람다 미적분은 직관형 이론의 근거지, 구성의 미적분, 종속형인 순수 람다 미적분(LF)이다.Berardi의 순수형 시스템에 대한 작업을 바탕으로 Henk Barendregt는 순수형 람다 미적분(단순히 타이핑된 람다 미적분, 시스템 F, LF 및 시공 미적분 포함)의 관계를 체계화하기 위해 람다 큐브를 제안했다.^{[citation needed]}

Some typed lambda calculi introduce a notion of subtyping, i.e. if ${\displaystyle A}$ is a subtype of ${\displaystyle B}$, then all terms of type ${\displaystyle A}$ also have type ${\displaystyle B}$. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and System F_<:.

지금까지 언급된 모든 시스템은 형식화되지 않은 람다 미적분을 제외하고 강하게 정상화되고 있다. 즉, 모든 계산이 종료된다.따라서 그들은 모든 튜링-컴퓨팅 기능을 설명할 수 없다.^[1]또 다른 결과로서 그들은 논리적으로 일관된다. 즉, 무인도 유형이 있다.그러나 강하게 정상화되지 않고 있는 활자형 람다 칼쿨리가 존재한다.예를 들어 모든 유형의 유형(유형 : 유형)을 가진 의존적으로 입력된 람다 미적분은 지라드의 역설로 인해 정규화되지 않고 있다.이 시스템은 또한 람다 큐브를 일반화하는 형식주의인 가장 단순한 순수형 시스템이다.플롯킨의 「계산 가능한 기능을 위한 프로그램 언어」(PCF)와 같이 명시적인 재귀 콤비네이터가 있는 시스템은 정상화는 아니지만, 논리로 해석할 의도는 없다.실제로 PCF는 프로그램들이 잘 행동하고 있지만 반드시 종료되는 것은 아니라는 것을 확실히 하기 위해 유형을 사용하는 원형 형태의 기능 프로그래밍 언어다.

프로그래밍 언어에 응용 프로그램

컴퓨터 프로그래밍에서 강하게 입력된 프로그래밍 언어의 루틴(기능, 절차, 방법)은 입력된 람다 표현식과 밀접하게 일치한다.

참고 항목

• 카파 미적분—고차 함수를 제외한 람다 미적분의 아날로그

메모들

추가 읽기

• Barendregt, Henk (1992). "Lambda Calculi with Types". In Abramsky, S. (ed.). Background: Computational Structures. Handbook of Logic in Computer Science. Vol. 2. Oxford University Press. pp. 117–309. ISBN 9780198537618.