연역 람다 미적분학

연역 람다 미적분학은 람다 용어를 수학적 표현으로 간주할 때 일어나는 일을 고려한다.정형화되지 않은 람다 미적분학에 대한 하나의 해석은 어떤 표현이 정상적인 형태일 때까지 축소를 수행함으로써 평가가 진행되는 프로그래밍 언어로서이다.이 해석에서 표현식이 결코 정상적인 형태로 줄어들지 않으면 프로그램은 결코 종료되지 않으며, 그 값은 정의되지 않는다.수학적 연역 체계로 간주되는 각각의 감소는 표현식의 가치를 변경하지 않을 것이다.그 표현은 그 표현의 축소와 같을 것이다.

역사

알론조 교회는 1930년대에 람다 미적분을 발명했는데, 원래 수학의 새롭고 단순한 기초를 제공하기 위해서였다.^[1][2]그러나 그것을 발명한 직후 주요한 논리적인 문제들은 람다 추상화의 정의로 확인되었다.클레인-로서의 역설은 람다 미적분학에서 리처드의 역설의 구현이다.^[3]하스켈 커리는 이 역설의 핵심 단계가 더 단순한 커리의 역설 구현에 사용될 수 있다는 것을 발견했다.이러한 역설의 존재는 람다 미적분이 연역계로서 일관되고 완전할 수 없다는 것을 의미했다.^[4]

Haskell Curry는 1941년에 병적인 (고려적인) 결합논리에 대해 공부했다.^[5]결합논리는 람다 미적분과 밀접하게 연관되어 있으며, 각각에 같은 역설들이 존재한다.

후에 람다 미적분은 프로그래밍 언어의 정의로 부활되었다.

소개

람다 미적분은 기능 프로그래밍 언어의 발전을 위한 모델이자 영감이다.이들 언어는 람다 추상화를 구현하며, 기능 및 유형의 적용과 연계하여 사용한다.

람다 추상화의 사용은 이후 다른 수학적 시스템에 내장되어 연역적 시스템으로 사용되면서 커리의 역설과 같은 여러 문제로 이어진다.문제는 람다 추상화의 정의와 람다 미적분학의 기본형식으로 함수의 정의와 사용과 관련이 있다.이 글에서는 이러한 문제점과 그 발생 방법에 대해 설명한다.

이것은 순수한 람다 미적분에 대한 비판은 아니며, 순수한 시스템으로서의 람다 미적분에 대한 비판은 여기서는 주요 주제가 아니다.문제는 람다 미적분학과 다른 수학적 계통의 상호작용으로 발생한다.문제를 인지하는 것은 경우에 따라 그들을 피할 수 있게 한다.

용어.

이 논의를 위해 람다 추상화는 수학의 추가 연산자로 추가된다.Boolean과 real과 같은 일반적인 도메인을 사용할 수 있을 것이다.이러한 영역에는 수학적 평등이 적용될 것이다.목적은 이 정의에서 어떤 문제가 발생하는지 보는 것이다.

함수 적용은 람다 미적분 구문을 사용하여 나타낼 것이다.그래서 곱셈은 점으로 표현될 것이다.또한, 몇몇 예에서는, let 표현이 사용될 것이다.

다음 표는 요약되어 있다.

이름	표기법
람다 추상화.	$\displaystyle \lambda v.y}$
f to x 함수 적용	$f\x}$
a by b의 곱하기	$a\cdot b}$
x 입력 y	${\displaystyle \propertname {let} x\propertname {in} y}$
수학적 평등	${\displaystyle m=n}$
베타 환원성 평등	${\displaystyle m\\\put {\put }{=}}\n}$

수학으로서의 람다 미적분 해석

수학적 해석에서 람다 항은 값을 나타낸다.Eta와 베타 감소는 표현 값을 변경하지 않는 연역적 단계다.

${\displaystyle \operatorname {eta-remedct} [X]=X}$

${\displaystyle \operatorname {beta-remission} [X]=X}$

수학으로서의 에타 감소

eta-remedact는 다음에 의해 정의된다.

${\displaystyle x\not \in \operatorname {FV}(f)\to \operatorname {eta-remissionct}[\lambda x.(f\ x)]=f}$

수학적 해석에 의하면

${\displaystyle \operatorname {eta-remedct} [X]=X}$

F를 변수로 삼는 건

$\displaystyle \lambda x.(f\ x)=f}$

$또는{\displaystyle }$ f ${\displaystyle \text{x}}$= ${\displaystyle y}$ ${\displaystyle f\ x=y}$을(를) 허용함으로써

$\displaystyle f\x=y=iff=\fda x.y.}$

${\displaystyle 이}$ 정의는 $\lambda {\displaystyle }$ ${\displaystyle x}$. y ${\displaystyle \lambda$ x$.y}$을(를) 방정식에서 f에 대한 솔루션으로$$ 정의한다.

$f\ x=y}$

수학으로서의 베타 감소

베타 환원제는,

${\displaystyle \probablename {displaystyle \computt}[(\da x.b)\z]b[x:=z]}$

그리고..

${\displaystyle \operatorname {beta-remission} [X]=X}$

그때

${\displaystyle(\data x.b)\z=b[x:=z]}$

이 규칙은 정량화된 변수의 인스턴스화에 의해 암시된다.만약

${\displaystyle \fall x:f\ x=y}$

${\displaystyle \text{f}}$ ${\displaystyle f\ z}$은(는) 계량화된 변수 x를 z로 인스턴스화한 y 식입니다.

${\displaystyle f\ z=y[x:=z]}$

그렇게

$(\displaystyle (\data x.y)\z=y[x:=z]}$

베타 축소는 eta 축소에 의해 암시되므로, 두 정의 사이에는 모순이 없다.

이변원칙과의 불일치

z를 부울로 하고, 그러면 우리는 아무런 해결책도 없이 방정식을 만들 수 있다.

$(\displaystyle z=\neg z}$

이 방정식을 재귀로 풀기 위해, 우리는 f에 의해 정의되는 새로운 함수를 도입한다.

${\displaystyle f\n=\neg(n\n)}$

여기서 n은 재귀 값을 보유하는 보조 변수다.$($우리는$display$ {\displaystyle $\neg }$이(가) 비 부울 인수가 주어지더라도 부울이 여전히$$ 반환되는 것으로 간주한다.)에타 삭감에 의해, 우리는 얻는다.

${\displaystyle f=\da x.\neg(x\ x)}$

그리고 나서,

$(\displaystyle {\displaysty}f\f&=(\da x.\neg(x\ x))(\data x.\neg(x\ x)))\\&=\neg(\da x.\neg(x\ x))(\da x.\neg(x\ x)))\\&=\neg(f\f)\end{aigned}}}$

그러면 f는 참도 거짓도 아니며, f가 부울 값이기 때문에(어떤 x에서든 f는 부울 $\neg {\displaystyle \mathrm{}}$ $){\displaystyle \neg (x\$ x$)\})$ 그러면 f는 참도 거짓도 아니라는 것을 알 수 있다. 또한 비논리적 값에 적용될 때 부정은 덜 타당하다는 것을 보여준다.

강도 대 확장 평등

연역계로서 람다 미적분학을 해석하기 위한 또 다른 어려움은 함수를 나타내는 람다 항으로서 값을 표현하는 것이다.형식에 맞지 않는 람다 미적분은 용어가 정상적인 형태가 될 때까지 람다 용어에 대한 감소를 수행하여 구현된다.평등에 대한 강도 높은^[6] 해석은 람다 항을 정상 형태로 줄이는 것이 람다 항의 값이라는 것이다.

이 해석은 람다 표현의 정체성을 그 구조로 간주한다.알파 컨버터블인 경우 두 람다 항은 같다.

함수 평등의 확장적 정의는 두 함수가 동일한 매핑을 수행하는 경우 두 함수가 동일하다는 것이다.

${\displaystyle f=g\iff(\all xf\ x=g\ x)}$

이것을 설명하는 한 가지 방법은 확장적 평등은 기능의 평등을 기술하고, 여기서 강화적 평등은 기능 구현의 평등을 기술한다.

평등의 확장적 정의는 강화적 정의와 동등하지 않다.이것은 아래의 예에서 볼 수 있다.이러한 불평등은 람다 용어를 값으로 간주함으로써 만들어진다.입력된 람다 미적분학에서는 이 문제를 우회한다. 왜냐하면 빌트인 타입은 표준적인 형태로 확장적 및 강도적 평등을 모두 갖는 값을 전달하기 위해 추가될 수 있기 때문이다.

예

산술에서 분배 법칙은 $2{\displaystyle \mathrm{}}$ ${\displaystyle \ast }$ (${\displaystyle }$r +${\displaystyle s}$ )${\displaystyle }$=${\displaystyle }$2 ${\displaystyle \ast }$ r +${\displaystyle 2}$ ${\displaystyle 2}$s ${\displaystyle 2**(r+s)=2*r+2*s}$을 내포하고 있다$.$ 왼쪽과 오른쪽 숫자의 교회 부호화를 사용하면 람다 용어로 나타낼 수 있다.

그래서 분배법에 따르면 두 가지 기능이 있다.

$\displaystyle \lambda r.\lambda s.2*(r+s)=\lambda r.\lambda s.2*r+2*s}$

교회 숫자의 함수로서 동등하다. (여기서 우리는 비형식 람다 미적분학의 기술적 약점에 직면한다: 어떤 함수의 영역을 교회 숫자로 제한할 방법이 없다.다음 논쟁에서 우리는 "모든" 람다 표현은 교회 숫자인 척하면서 이 어려움을 무시할 것이다.)교회 숫자가 숫자의 만족스러운 구현을 제공했다면 분배법을 적용해야 한다.

$♪ displaystyle {\displaysty}\justda r.\lambda s.\operatorname {mult} \ 2\(\multname {plus} \ r\ s)&=\bigda r.\lambda s.\criptname {plus} \(\multname {mult} \ 2\ r)\(\multname {mult} \ 2\s)\\\\scriptstyle \boda r.\lambda s.(\lambda m.\lambda n.\lambda f.m\ (n\ f)\\ (\lambda f.\lambda x.f\ (f\ x)\ (\lambda m).\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)\ r\s)}&={\scriptstyle \lambda r.\lambda s.(\lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)\ (\lambda m).\lambda n.\lambda f.m\ (n\ f)\\ (\lambda f.\lambda x.f\ (f\ x)\ r)\ (\lambda m).\lambda n.\lambda f.m\ (n\ f)\\ (\lambda f.\lambda x.f\ (f\ x)\s)}\\\\\chbda r.\lambda s.\lambda f.\lambda x.r\ f\ (s\ f\ (r\ f\ x)))&=\ftda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ x)))\end{정렬}}}$

베타라는 두 용어는 비슷한 표현으로 줄어든다.여전히 그들은 알파 컨버터블도, 심지어 eta 컨버터블도 아니다. (두 용어가 이미 eta-long 형태이기 때문에 후자가 뒤따른다.)그래서 평등에 대한 강도 높은 정의에 따르면 그 표현은 같지 않다.그러나 만약 두 기능이 동일한 교회 숫자에 적용된다면, 그들은 분배법에 의해 동일한 결과를 낳는다. 따라서 그들은 확장적으로 평등하다.

이것은 람다 기간의 강도 값이 확장적으로 유효한 변환 하에서 변경될 수 있다는 것을 의미하기 때문에 중요한 문제다.이 문제에 대한 해결책은 오메가 룰을 도입하는 것이다.

• 모든 람다-엑스포션 t에 $대해{\displaystyle }$ f ${\displaystyle \text{t}\underset{}{}}$= ${\displaystyle \underset{}{\beta }}$ g ${\displaystyle \text{t}}$ ${\displaystyle$ f$\\t\\\{=}\beta }},$$f{\displaystyle \underset{}{}}$= ${\displaystyle \underset{}{\beta }}$ ${\displaystyle g}$ ${\displaystyle f\$ {\$underset {\data}{=}\}\g}$.

우리 상황에서 '올 람다 엑스포션'은 '모든 교회 숫자'를 의미하기 때문에 표준적인 의미에서도 오메가 룰이다.오른쪽의 베타 축소에 의한$$ f ${\displaystyle \text{t}}$ =${\displaystyle \underset{\beta }{}}$ (${\displaystyle \beta }$ ${\displaystyle x}$ .${\displaystyle \text{f}}$ ${\displaystyle x}$) t ${\displaystyle f\$ $\\\\\nderset {\$beta $}{=}\\$ (\$lambda x.f\ x)\\}$이(가)이므로 오메가 규칙은 eta 규칙을 함축한다는 점에 유의한다.

정리 도메인 설정

람다 추상화는 기능의 기능이다.자연스러운 단계는 람다 추상화에 대한 도메인을 모든 기능의 집합으로 정의하는 것이다.

도메인 D에서 범위 R에 이르는 모든 기능의 집합은 K in에 의해 주어진다.

$(\displaystyle f\in K\iff (\forall x:x\in D\implies f\ x\in R)}$

그리고 기능들의 모든 기능들의 집합에 대한 (상상적)의 정의는 F in에 의해 주어진다.

$F\iff(\forall x:x\in F\implies f\x\in F)}$

이 정의는 자명적인 집합론에서는 공식화될 수 없으며, 이 순진한 방정식은 비록 집합 이론으로 쓰여질 수 있다 하더라도 해답이 없다.

이제 람다 미적분은 베타 감소와 에타 감소에 의해 정의된다.감소를 동등함을 정의하는 것으로 해석하면 람다 미적분학에 대한 암묵적 영역을 제공한다.규칙은,

• 모든 람다 추상화는 하나의 가치를 가지고 있다.
• 람다 항의 베타 축소는 같은 값을 갖는다.
• 람다 항의 eta 축소는 같은 값을 갖는다.
• 알파 컨버터블 람다 항은 동일하다.
• [오메가 법칙이 존재한다면] "오메가 등가" 람다 항은 같다.
• 위의 규칙으로 두 람다 용어가 같음을 보여줄 수 없다면, 그들은 같지 않다.

만약 두 개의 람다 용어가 정상 형태로 축소될 수 있다면, Church-Roser 정리는 만약 그들의 정상적인 형태가 알파 컨버터블이라면 그들이 동등하다는 것을 보여주기 위해 사용될 수 있다.

두 항 중 하나 또는 둘 다 정규화되지 않은 경우 등가성의 불분명한 점은 일반적으로 두 람다 항이 동일한지 여부를 판별할 알고리즘이 없다는 것을 보여준다.일반적으로 이것은 람다 미적분 영역의 뚜렷한 요소가 무엇인지 알 수 없게 만든다.

예:솔루션 없음 → 하나의 솔루션

예를 들어 $x{\displaystyle }$ =${\displaystyle \mathrm{\neg }}$ ${\displaystyle x}$ ${\displaystyle x=\neg x}$ 방정식은 Church 인코딩을 사용하여 다음과 같이$$ Curry의 Y 콤비네이터를 사용하여 코드화할 수 있다.

${not} _{1}=\da p.\lambda a.\lambda b.p\ b\ a}$

$[\displaystyle (\displayda x.f\ (x\x\)\\\da x.f\ (x\ x))(\displayda p.\lambda a.\lambda b.p\ b\ a)}$

그리고 그 재귀는,

$(\displaystyle(\displaystyle)(\data x.)(\da p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\ (\\da x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)}}$

$(\displaystyle)(\da p.\lambda a.\lambda b.p\ b\ a)\(\\da x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\ (\\da x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)}}$

$\displaystyle \lambda a.\lambda b.(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\ (\\da x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\ b\ a}$

...

$\displaystyle \lambda a.\lambda b.(\lambda a.\lambda b.(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\ (\\da x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\b\b\ a}$

… (이후 에타감소)

$(\displaystyle(\displaystyle)(\data x.)(\da p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)\ (\\da x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)}}$

그것은 첫 번째 줄이고 무한정 반복될 것이다.그 표현은 결코 정상적인 형태로 줄어들지 않는다.그러나 감소에서 모든 람다 항은 동일한 값을 나타낸다.이 값은 참 또는 거짓에 대한 인코딩과는 구별된다.부울 영역의 일부는 아니지만 람다 미적분 영역에 존재한다.

예:다중 솔루션 → 단일 솔루션

분할된 숫자와 서명된 숫자를 사용하여 Y 결합기를 사용하여 정수 제곱근을 나타내는 식을 정의할 수 있다.교회 인코딩은 또한 합리적이고 실제적인 숫자로 더 확장될 수 있으며, 그래서 실제 제곱근을 정의할 수 있다.Church-Turing 논문은 계산 가능한 연산자(및 그 연산자)가 람다 미적분학으로 표현될 수 있음을 암시한다.

그런 인코딩을 사용하면

${\displaystyle x^{2}=n\오른쪽 화살표 x={\frac {n}{x}}\오른쪽 화살표 f\={\frac {n}{x}}\land Y\f=x}$

분할의 구현을 이용하여,

${\displaystyle Y(\operatorname {divide}n)}$

n이 0이 아닌 경우, 서명된 숫자의 도메인에서 두 개의 값을 나타낸다.그러나 람다식이라 람다 미적분학 영역에는 하나의 값만 있다.이 람다 용어의 베타 감소는 결코 정상적인 형태에 도달하지 않는다.그러나 값을 나타내므로 람다 미적분 영역의 단일 값은 서명된 숫자 영역의 두 값을 나타낸다.

참고 항목

• 람다 미적분학
• 표현으로 하자
• 교회 부호화

참조