람다무 미적분

수학적 논리와 컴퓨터 과학에서 람다무 미적분은 M. 패리고트가 도입한 람다 미적분의 연장이다.^[1]그것은 두 개의 새로운 연산자, 즉 μ 연산자(계산가능성 이론에서 발견되는 μ 연산자와 모달 μ- 미적분의 μ 연산자 둘 다 완전히 다르다)와 브래킷 연산자를 소개한다.증명 이론적으로, 그것은 고전적인 자연 추론의 적절한 형태를 제공한다.

이 확장된 미적분학의 주요 목표 중 하나는 고전적 논리에서 이론에 해당하는 표현을 묘사할 수 있는 것이다.커리-하워드 이소모르피즘에 따르면 람다 미적분 그 자체로는 직관적 논리로만 이론들을 표현할 수 있고, 몇 가지 고전적 논리적인 이론들은 전혀 쓸 수 없다.그러나 이러한 새로운 연산자로는 예를 들어 Peirce의 법칙의 유형을 가진 용어를 쓸 수 있다.

의미론적으로 이러한 연산자는 기능 프로그래밍 언어에서 발견되는 연속성에 해당한다.

형식 정의

우리는 람다-무 미적분학의 맥락에서 하나를 얻기 위해 람다 표현의 정의를 증가시킬 수 있다.람다 미적분학에서 발견되는 세 가지 주요 표현은 다음과 같다.

1. V(V) 변수, 여기서 V는 식별자임.
2. λV.E, 추상화, 여기서 V는 식별자, E는 람다 식이다.
3. (E E′), 여기서 E와 E'는 람다식이다.

자세한 내용은 해당 문서를 참조하십시오.

람다-무 미적분학에는 기존의 λ-변수 외에도 μ변수들의 뚜렷한 집합이 포함되어 있다.이러한 μ-변수는 임의의 하위 단어의 이름을 짓거나 동결하는 데 사용될 수 있으며, 나중에 이러한 이름에 대해 추상화할 수 있다.용어 집합에는 이름 없는(모든 전통적인 람다 표현은 이와 같은 종류)과 명명된 용어가 포함되어 있다.람다-무 미적분학에 의해 첨가되는 용어는 다음과 같은 형식이다.

1. [α]t는 명명된 용어로서, 여기서 α는 μvariable이고 t는 이름 없는 용어다.
2. (μ α. E)는 이름 없는 용어로, 여기서 α는 μ-변수, E는 명명된 용어다.

축소

람다무 미적분학에서 사용되는 기본 감량 규칙은 다음과 같다.

논리적 감소

${\displaystyle(\displaystyle)(\data x.u)v\;\light _{c}\;u[v/x]}$

구조 축소

${\displaystyle (\mu \b)v\;\light _{c}\;\mu \u\left[\mu \wv]/[\mu \w\w\right]}}$

이름 바꾸기

${\displaystyle [\displaystyle ]\mu \mu .u\;\blineight _{c}\;u[\bu]/\bu ]}$

η저감에 상당하는 것

${\displaystyle \mu \alpha.$u에서 자유롭게 발생하지 않는 α에 대해$$$[\properties ]u\;\light _{c}\;u}$

이 규칙들은 미적분을 합치하게 한다.비록 이것이 합성의 희생이 되겠지만, 우리에게 정상적인 형태에 대한 더 강력한 개념을 제공하기 위해 추가적인 감소 규칙이 추가될 수 있다.

참고 항목

• 제어 기능이 있는 람다 칼쿨리의 형식 일반화를 위한 고전적인 순수 유형 시스템

참조

외부 링크

• 람다무 더 얼티밋에 대한 관련 논의