결합 논리학

결합논리는 수학논리에서 정량화된 변수의 필요성을 없애기 위한 표기법이다. 모세 쇤핀켈과^[1] 하스켈 커리에 의해 도입되었으며,^[2] 최근에는 컴퓨터 과학에서 연산의 이론적 모델로서 뿐만 아니라 기능 프로그래밍 언어의 설계의 기초로서도 활용되고 있다. 그것은 기능들을 구축하고 변수에 대한 언급은 특히 술어 논리에서 제거하는 유사한 방법을 제공한다는 생각으로 1920년에 쇤핀켈에 의해 소개된 결합기를 기반으로 한다. 콤비네이터는 함수 어플리케이션과 초기에 정의된 콤비네이터만을 사용하여 인수의 결과를 정의하는 고차 함수다.

수학에서는

결합논리는 원래 논리학에서 정량화된 변수의 역할을 명확히 하는 '사전논리학(pre-logic)'으로, 본질적으로 그것들을 제거함으로써 의도되었다. 정량화된 변수를 제거하는 또 다른 방법은 Quine의 술어 펑터 논리다. 결합논리의 표현력이 전형적으로 1차 논리학의 표현력을 능가하는 반면, 술어 펑터 논리의 표현력은 1차 논리학의 표현력과 동일하다(Quine 1960, 1966, 1976).

전투적 논리의 창시자인 모세 쇤핑클은 1924년 논문 이후 전투적 논리에 대해 아무것도 발표하지 않았다. 하스켈 커리는 1927년 말 프린스턴 대학에서 강사로 일하면서 콤비네이터를 재발견했다.^[3] 1930년대 후반 알론조교회와 프린스턴 대학의 제자들은 기능적 추상화에 대한 경쟁적인 형식주의인 람다 미적분을 발명했는데, 이것은 결합적 논리보다 더 인기 있는 것으로 증명되었다. 이러한 역사적 우발상황의 결론은 이론 컴퓨터 과학이 1960년대와 1970년대에 전투적 논리에 관심을 갖기 시작할 때까지, 이 문제에 관한 거의 모든 작업은 하스켈 커리와 그의 제자들이나 벨기에의 로버트 페이스에 의해 이루어졌다는 것이다. 커리와 페이(1958)와 커리 외 연구진(1972)은 결합 논리의 초기 역사를 조사한다. 결합논리와 람다 미적분학을 함께 다루는 좀 더 현대적인 방법은, 1960년대와 1970년대에 결합논리를 위해 고안된 다나 스콧의 모델을 검토하는 ^[4]바렌트레트의 책을 보라.

컴퓨팅에서

컴퓨터 과학에서, 결합 논리는 계산가능성 이론과 증명 이론에 사용되는 계산의 단순화된 모델로 사용된다. 단순함에도 불구하고, 전투적 논리는 연산의 많은 필수적인 특징들을 포착한다.

결합논리는 람다 미적분학의 변형으로 볼 수 있는데, 람다 표현식(기능적 추상화를 나타냄)은 자유변수가 없는 원시함수인 제한된 결합기 집합으로 대체된다. 람다 식을 콤비네이터 식으로 변환하기 쉽고 콤비네이터 축소가 람다 축소보다 훨씬 간단하다. 따라서 전투적 논리는 일부 엄격한 기능 프로그래밍 언어와 하드웨어를 모델링하는 데 사용되어 왔다. 이 견해의 가장 순수한 형태는 프로그래밍 언어인 Unlambda인데, 유일한 원형은 문자 입력/출력으로 증강된 S와 K 콤비네이터이다. 비록 실용적인 프로그래밍 언어는 아니지만, 운람바다는 이론적인 흥미가 있다.

결합논리는 다양한 해석을 할 수 있다. 커리의 많은 초기 논문들은 전통적인 논리에 대한 공리 세트를 결합 논리 방정식으로 변환하는 방법을 보여주었다(Hindley and Merededes 1990). 1960년대와 1970년대의 다나 스콧은 모델 이론과 전투적 논리와 결혼하는 법을 보여주었다.

람다 미적분 요약

람다 미적분은 람다-단어라고 불리는 물체와 관련이 있는데, 이 물체는 다음과 같은 세 가지 형태의 문자열로 나타낼 수 있다.

• ${\displaystyle v}$
• $\displaystyle \lambda v.E_{1}:{1}$
• ${\displaystyle(E_{1}E_{2})}$

여기서 $v{\displaystyle }$ ${\displaystyle v}$은(는) 미리 정의된 무한 변수 이름 집합에서 가져온 변수 이름이며, $E{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$}:{1$}$ $및$ ${\displaystyle {E\mathrm{}}_{}}$ 2$${\$displaystyle E_{2}}$은 람다-단어다.

$\lambda {\displaystyle }$ ${\displaystyle v}$. ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$ v $형식$의 용어$.$$E_{1}:{$1}은(는) 추상화라고 불린다$$. 변수 v는 추상화의 공식 매개변수라고 하며 ${\displaystyle {E\mathrm{}}_{}}$ 1 ${\$}는$$ 추상화의 본체다. 용어 $\lambda {\displaystyle }$ ${\displaystyle v}$. E ${\displaystyle {1\mathrm{}}_{}}$ ${\$$E_{1$}는 인수에 적용된 형식 매개 변수 v를 인수에 바인딩한 다음 결과 값 E ${\displaystyle {1\mathrm{}}_{}}$${\$}를 계산하는 함수를 나타내며$$$,$ 즉, v가 발생할 때마다 인수로 대체되는 E $1{\displaystyle {}_{}}$ ${\$}를$$반환한다.

형식$({\displaystyle {E1\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$) ${\displaystyle(E_{1}E_{2})$의 용어를 애플리케이션이라고 한다$$. 애플리케이션 모델 함수 호출 또는 실행: $E{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$1}로$$대표되는 함수를 호출하여$$ $E{\displaystyle {}_{}}$ 2 ${\$2}}을 인수로 하고 결과를$$ 계산한다. $E{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$응용프로그램이라고도 함)이 추상적인 경우, 용어는 다음과 같이 줄일 수 있다. ${\displaystyle E_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ ${\$ 인수는 E ${\displaystyle {1\mathrm{}}_{}}$ ${\$$1$}의 공식 매개변수 대신$$ $E{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$}의 본문으로 대체될 수 있으며, 그 결과는 기존 용어와 동등한 새로운 람다 용어가 된다. 람다 용어에 형식의 하위 단어가 없는 경우$({\displaystyle }$ (${\displaystyle \lambda }$ ${\displaystyle v.}$ ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}{}_{}}$)${\displaystyle ((\lambda v)).$$E_{1}E_{2}}$ 그러면$$ 줄일 수 없으며, 정상적인 형태라고 한다.

$E{\displaystyle [}$ ${\displaystyle v}$ ${\displaystyle :=}$ ${\displaystyle ]}$ ${\displaystyle E[v:=a]}$라는 표현은 E라는 용어를 사용하고 그 안에서 발생하는 모든 자유 발생을 a로 대체한 결과를 나타낸다$$. 그래서 우리는 쓴다.

$(\displaystyle)(\da v.E)a)\오른쪽 화살표 E[v:=a]}$

관례에 따라$,{\displaystyle }$ 우리는 (${\displaystyle b}$c${\displaystyle }$) {\$displaystyle ($abc${\displaystyle )\}}$을${\displaystyle (}$를) (${\displaystyle b}$)$$c ) {\$displaystyle$((ab)$c)}$의 속기로 받아들인다(즉, 애플리케이션은 연관성이 남아 있다).

이러한 감소의 정의의 동기는 모든 수학 함수의 본질적인 행동을 포착하기 때문이다. 예를 들어, 숫자의 제곱을 계산하는 함수를 생각해 보십시오. 우리는 쓸지도 모른다.

x의 제곱은 ${\displaystyle x}$ ${\displaystyle \ast }$ x ${\displaystyle$ x$*x}$이다.

(" ${\displaystyle }$ ${\displaystyle *}$"을(를) 사용하여 곱셈을 나타냄) x는 함수의 공식 매개변수 입니다. 예를 들어, 3과 같이 특정 인수에 대한 제곱을 평가하기 위해, 공식 매개변수 대신 정의에 삽입한다.

3의 제곱은 ${\displaystyle 3}$ ${\displaystyle \ast }$ 3 $[\displaystyle$ 3$*3}$

$결과표현{\displaystyle \mathrm{}}$ 3${\displaystyle 3}$ 3$${\$displaystyle 3*3$을(를) 평가하려면 곱셈과 숫자 3에 대한 지식에 의존해야 할 것이다. 어떤 계산도 단순히 적절한 원시적 인수에 대한 적절한 함수의 평가의 구성이기 때문에, 이 간단한 대체 원리는 계산의 필수적인 메커니즘을 포착하기에 충분하다. 더욱이 람다 미적분학에서는 외부적으로 정의된 원시 연산자나 상수 없이도 '3'과 ' '${\displaystyle$ $*\}\text{'}$와 같은 개념을 나타낼 수 있다. 람다 미적분학에서 용어를 식별할 수 있는데, 적절히 해석하면 숫자 3처럼 행동하고 곱셈 연산자인 Q.v. Church 인코딩처럼 행동한다.

람다 미적분은 계산을 위해 많은 다른 그럴듯한 모델(Turing machine 포함)과 연산적으로 동등한 것으로 알려져 있다. 즉, 이러한 다른 모델에서 달성할 수 있는 모든 계산은 람다 미적분으로 표현될 수 있고, 그 반대의 경우도 마찬가지다. Church-Turing 논문에 따르면, 두 모델 모두 가능한 계산을 표현할 수 있다.

람다-미적분이 변수에 대한 용어의 단순한 텍스트 대체에 기초한 기능 추상화와 적용의 단순한 개념만을 사용하여 상상할 수 있는 계산을 나타낼 수 있다는 것은 아마도 놀랄 것이다. 그러나 더욱 주목할 만한 것은 추상화는 필요조차 없다는 점이다. 결합 논리학은 람다 미적분학에 해당하는 계산 모델이지만 추상화는 없다. 이것의 장점은 대체의 의미론을 매우 주의 깊게 명시해야 가변 포획 문제가 발생하지 않기 때문에 람다 미적분학의 표현 평가가 상당히 복잡하다는 것이다. 대조적으로, 대체에 대한 개념이 없기 때문에, 전투적 논리로 표현들을 평가하는 것은 훨씬 더 간단하다.

콤비네이션 칼쿨리

추상화는 람다 미적분에서 함수를 제조하는 유일한 방법이기 때문에 결합 미적분에서 어떤 것이 그것을 대체해야 한다. 추상화 대신에, 결합 미적분은 다른 기능들이 만들어질 수 있는 제한된 원시 기능들을 제공한다.

결합 용어

결합 용어는 다음 형식 중 하나를 가진다.

구문	이름	설명
x	변수	결합 용어를 나타내는 문자 또는 문자열.
P	원시함수	결합기 기호 I, K, S 중 하나.
(M N)	적용	인수에 함수 적용. M과 N은 전투용어다.

원시 함수는 결합기 또는 람다 용어로 볼 때 자유 변수를 포함하지 않는 함수다.

공지를 단축하기 위해 일반적인 규약은${\displaystyle }$(${\displaystyle {E1\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {3\mathrm{}}_{}}$.${\displaystyle }$. ${\displaystyle {}_{}}$ ${\displaystyle n_{}}$) ${\displaystyle (E_{1}E_{2}E_{3}...$$E_{n},$ 또는$$$E{\displaystyle {}_{}}$ 1 ${\displaystyle {E\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {E\mathrm{}}_{}}$ 3${\displaystyle }$. .${\displaystyle }$. ${\displaystyle E_{}}$ ${\displaystyle {}_{}}$ ${\$$E_{n}}$은$(.$ .${\displaystyle }$. .${\displaystyle }$(${\displaystyle }$( ${\displaystyle {E1\mathrm{}}_{}}$ ${\displaystyle {E\mathrm{}}_{}}$ 2${\displaystyle {}_{}}$) ${\displaystyle {}_{}}$ ${\displaystyle {}_{}{}_{}}$)${\displaystyle (...(E_{1}E_{2})$이라는 용어를 나타낸다.$E_{3}...$$E_{n}}$. 이것은 람다 미적분학의 복수 적용과 같은 일반적 관례(좌우 연관성)이다.

결합논리의 감소

결합 논리학에서는 각각의 원시 결합자는 형태의 축소 규칙을 가지고 온다.

(P x₁ ... x_n) = E

여기서 E는 {x₁ ... 집합의 변수만 언급하는 용어다. x_n}. 원시 콤비네이터가 함수로서 작용하는 것은 이와 같은 방식이다.

결합기의 예

조합자의 가장 간단한 예는 I로 정의되며, 다음과 같이 정의된다.

(I x) = x

모든 용어에 대해 x. 또 다른 간단한 조합자는 K인데, K는 상수 기능을 제조한다: (K x)는 어떤 주장에도 x를 반환하는 기능이다. 그래서 우리는 이렇게 말한다.

((K x) y) = x

x와 y의 모든 용어에 대해. 아니면, 다중 적용에 대한 관례에 따라,

(K x y) = x

세 번째 콤비네이터는 S로, 응용 프로그램의 일반화된 버전이다.

(S x y z) = (x z(y z))

S는 각각에 먼저 z를 대체한 후 y에 x를 적용한다. 또는 다른 방법으로, x는 환경 z 안에서 y에 적용된다.

S와 K가 주어진다면 다른 두 개로부터 건설될 수 있기 때문에 나 자체는 불필요하다.

((S K) x)

= (S K K x)

= (K x (K x)

= x

어떤 용어에 대해서도 x. 어떤 x에 대해서도 (S K) x = (I x)는 (S K K) 자체가 I과 같지 않다는 점에 유의하십시오. 우리는 조건이 확장적으로 동등하다고 말한다. 확장적 평등은 함수 평등이라는 수학적 개념을 포착한다. 즉, 두 함수가 항상 동일한 인수에 대해 동일한 결과를 낸다면 두 함수는 동일하다는 것이다. 대조적으로, 용어 자체는 원시 결합자의 감소와 함께 기능의 강도적 평등 개념을 포착한다: 두 가지 기능은 원시 결합체의 확장에 이르기까지 동일한 구현을 가지고 있어야만 동일하다는 것이다. 아이덴티티 함수를 구현하는 많은 방법들이 있다; (S K K)와 나는 이러한 방법들 중 하나이다. (S K S)는 아직 또 다른 것이다. 우리는 확장적 평등을 나타내기 위해 등가라는 단어를 사용할 것이며, 동일한 조합 용어에 대해 동등하게 예약할 것이다.

보다 흥미로운 결합체는 재귀 구현에 사용할 수 있는 고정점 결합기 또는 Y 결합기다.

S-K 기준의 완전성

S와 K는 어떤 람다 용어와 확장적으로 동일한 결합체를 생산하기 위해 구성될 수 있으며, 따라서 Church의 논문에 의해 어떤 계산 가능한 기능에도 적용될 수 있다. 그 증거는 임의의 람다 용어를 등가 결합체로 변환하는 변환 T[ ]를 제시하는 것이다.

T[ ]는 다음과 같이 정의할 수 있다.

1. T[x] => x
2. T[(E₁ E₂)] => (T[E₁] T[E₂])
3. T[λx.E] =>(K T[E]) (E에서 x가 자유롭지 않은 경우)
4. T[λx.x] => I
5. T[λx.λy]E] => T[λ]T[basy.E] (E에서 x가 자유롭게 발생하는 경우)
6. T[λx.(E₁ E₂)] =>(S T[λλ])E₁] T[λ]E₂]) (X가 E₁ 또는 E₂에서 무료로 발생하는 경우)

주어진 T[ ]는 형식이 올바른 수학적 함수가 아니라 다음과 같은 용어라는 점에 유의하십시오. 비록 결국 결합자를 산출하지만, 변환은 규칙(5)을 통해 람다 용어나 결합자가 아닌 중간 식을 생성할 수 있다.

이 과정은 추상화 제거라고도 알려져 있다. 이 정의는 완전하다: 모든 람다 표현은 정확히 다음 규칙 중 하나를 따른다(위의 람다 미적분 요약 참조).

변수와 응용에서 빌드된 E 식을 취하여 [x]E x = E가 보유하는 것과 같이 변수 x가 자유롭지 않은 조합식[x]E를 생성하는 브라켓 추상화 과정과 관련이 있다. 브래킷 추상화를 위한 매우 간단한 알고리즘은 다음과 같은 표현 구조에서 유도에 의해 정의된다.^[5]

1. [x]y :=Ky
2. [x]x := I
3. [x](E₁ E₂) := S([x]E₁)([x]E₂)

브라켓 추상화는 브라켓 추상화 알고리즘을 사용하여 람다-수축을 해석함으로써 람다 용어에서 콤비네이터 표현으로 번역을 유도한다.

람다 항을 등가 조합 항으로 변환

예를 들어, 람다 용어 λx.λy.(y x)를 조합 용어로 변환한다.

T[λx.λy.(yx)]

= T[λx.T[λy.(y x)]] (5)

= T[λx.(S T[λy.y] T[λy.x]])] (6)

= T[tx.(S I T[[y.x]])](4)

= T[tx.(S I (K T[x]))]](3)

= T[tx.(S I (K x)))] (1)

= (S T[λx.(S I)] T[λx.(K x)]) (6)

= (S (K (S I)) T[λx.(K x)]) (3)

= (S (K (S I))(S T[[x.K] T[λx.x]) (6)

= (S (K (S I))(S (K) T[[x.x]])(3)

= (S (S (S I))(S (K) I)) (4)

이 조합 용어를 x와 y의 두 가지 용어에 적용하면('오른쪽에서부터'로 줄임말처럼 줄임으로써) 다음과 같이 감소한다.

(S (K (SI))(S (K) I) x y)

= (K (S I) x (S (K) I x) y)

= (S I (S (K) I x) y)

= (I y (S (K) I x y))

= (y (S (K) I x y))

= (y (K K x (I x) y))

= (y (K (I x) y))

= (y)(I x)

= (y x)

결합적 표현, (S (S (S I)) (S (K) I)))는 람다 용어인 λx.λy.(y x)보다 훨씬 더 길다. 이게 대표적이다. 일반적으로 T[ ] 구조는 길이 n의 람다 항을 길이 θ(n³)의 결합 항으로 확장할 수 있다.^[6]

T[ ] 변환 설명

T[ ] 변환은 추상화를 없애려는 욕구에 의해 동기 부여된다. 두 가지 특별한 경우인 규칙 3과 4는 사소한 것이다: λx.x는 분명히 I과 동등하고, λx는 λx와 같다.E에서 x가 자유로워 보이지 않으면 E는 분명히 (K T[E])와 동일하다.

앞의 두 가지 규칙도 간단하다. 변수 자체가 변환되고, 결합적 용어로 허용된 응용 프로그램은 응용 프로그램과 인수를 결합체로 변환하는 것만으로 결합자로 변환된다.

관심있는 것은 규칙 5와 6이다. 규칙 5는 단순히 복잡한 추상화를 결합체로 전환하기 위해서는 우선 그 몸을 결합체로 전환한 다음 추상화를 제거해야 한다고 말한다. 규칙 6은 실제로 추상화를 제거한다.

λx.(E₁ E₂)는 주장을 취하여 a라고 하고, 이를 x 대신 람다어(E₂ E into)로 대체하여 양보(E₂ E[)[x : = a]하는 함수다. 그러나 x 대신 a를 (E₁ E₂)로 대체하는 것은 E₁과 E₂ 둘 다로 대체하는 것과 같기 때문에,

(E₁ E₂)[x := a] = (E₁[x := a] E₂[x := a])

(λx. (E₁ E₂) a) = (λx.E₁ a) (λx).e₂ a)))

= (S λx).E₁ λx.E₂ a)

= ((S λx).E₁ λx.E₂) a)

확장적 평등에 의해,

λx.(E₁ E₂) = (S λx)E₁ λx.E₂)

따라서 λx.(E₁ E₂)에 해당하는 콤비네이터를 찾으려면 (S λx)에 해당하는 콤비네이터를 찾으면 충분하다.E₁ λx.E₂) 및

(S T[λ].E₁] T[λ]E₂])

분명히 그 계산에 들어맞다 E₁과 E₂ 각각은 (E₁ E₂)보다 엄격히 적은 수의 응용 프로그램을 포함하고 있으므로, 재귀는 변수 또는 λx.E 형식의 용어인 람다 용어로 종료되어야 한다.

변환의 단순화

η 축소

T[ ] 변환에 의해 생성되는 결합기는 : 감소 규칙을 고려한다면 더 작게 만들 수 있다.

T[118x.(E x)] = T[E](E에서 x가 자유롭지 않은 경우)

λx.(E x)는 인수, x를 취하여 거기에 기능 E를 적용하는 함수로서, 이것은 기능 E 자체와 확장적으로 동일하다. 따라서 E를 조합형식으로 변환하는 것으로 충분하다.

이러한 단순화를 고려하여 위의 예는 다음과 같다.

T[λx.λy.(y x)]

= ...

= (S (K (S I)) T[λx.(K x)]))

= (S (K (S I)) K) (η-축소)

이 결합기는 이전보다 긴 결합기와 동일하다.

(S (K (S I) K x y)

= (K (S I) x (K x) y)

= (S I (K x) y)

= (I y(K x y))

= (y)(K x y)

= (y x)

마찬가지로 T[ ] 변환의 원본은 ID 함수 functionf를 변형시켰다.λx. (f x) in (S (K S) (S (K) I) (K I))). η-축소규칙으로 λf.λx.(f x)는 I로 변한다.

원포인트 베이시스

모든 결합기를 람다 용어와 확장적으로 구성할 수 있는 원 포인트 베이스가 있다. 이러한 근거의 가장 간단한 예는 다음과 같은 {X}이다.

X ≡ λx.(xS)K)

다음을 검증하는 것은 어렵지 않다.

X(X(X)) ^β= K 및

X(X(X(X(X)))) ^β= S.

{K, S}이(가) 기본이기 때문에 {X}도 기본이 되는 것을 따른다. 이오타 프로그래밍 언어는 X를 유일한 콤비네이터로 사용한다.

원포인트 기준의 또 다른 간단한 예는 다음과 같다.

X' ≡ xx.(x K S K)와

(X' X') X' ^β= K 및

X' (X' X') =^β S

사실 그러한 근거는 무한히 많이 존재한다.^[7]

콤비네이터 B, C

쇤핀켈의 논문에는 S와 K 외에도 현재 B와 C라고 불리는 두 개의 콤비네이터가 포함되었으며, 다음과 같은 감소가 있었다.

(C f g x) = ((f x) g)

(B f g x) = (f (g x))

그는 또한 S와 K:만을 사용하여 그것들을 차례대로 표현할 수 있는 방법을 설명한다.

B = (S (K S) K)

C = (S (S (S (K S) K)) S) (K K))

이러한 결합자는 술어 논리학이나 람다 미적분을 결합기 표현으로 변환할 때 매우 유용하다. 그것들은 또한 커리에 의해 사용되었고, 훨씬 후에 데이비드 터너에 의해 사용되었는데, 그의 이름은 그들의 컴퓨터 사용과 관련이 있다. 그것들을 사용하면 다음과 같이 변환 규칙을 확장할 수 있다.

1. T[x] ⇒ x
2. T[(E₁ E₂)] ⇒ (T[E₁] T[E₂])
3. T[λx.E] ⇒ (K T[E]) (E에서 x가 자유롭지 않은 경우)
4. T[λx.x] ⇒ I
5. T[λx.λy]E] ⇒ T[λ].T[λy.E] (E에서 x가 무료인 경우)
6. T[λx.(E₁ E))] ⇒ (S T[λλ]).E₁] T[λ]E₂]) (X가 E₁과 E₂에서 모두 무료인 경우)
7. T[λx.(E₁ E₂)] ⇒(C T[λ]).E₁] T[E₂] (X가 E₁에서는 무료지만 E₂에서는 무료인 경우)
8. T[λx. (E₁ E₂)] ⇒ (B T[E₁] T[λ] T[λ]E₂]) (X가 E₂에서는 무료지만 E₁에서는 무료인 경우)

B와 C 콤비네이터를 사용하여 λx.λy(y x)의 변환은 다음과 같다.

T[λx.λy.(y x)]

= T[λx.T[λy.(y x)]]

= T[tx.(C T[ ty.y] x)] (규칙 7)

= T[tx.(C I x)]

= (C I)( (-축소)

= $C{\displaystyle {\mathbf{}}_{}}$ ${\displaystyle {}_{}}$ ${\$$기존{\displaystyle {\mathbf{}}_{}}$ 표준 표기법: X ${\displaystyle {}_{}}$= X ${\displaystyle \mathbf{I}}$ ${\$$_{*}=\mathbf {XI}$ )

= $I{\displaystyle {\mathbf{}}^{}}$ ${\displaystyle {}^{}}$ ${\$기존 표준 표기법: $X{\displaystyle {\mathbf{}}^{}}$ ${\displaystyle {}^{}}$= C ${\displaystyle \mathbf{X}}$ ${\$ )

그리고 실제로 (C I x y)는 (y x)로 감소한다.

(C I x y)

= (I y x)

= (y x)

여기서의 동기는 B와 C가 S의 한정된 버전이라는 것이다. S는 어떤 값을 취하여 응용 프로그램을 수행하기 전에 응용 프로그램과 이의 주장으로 대체하는 반면에, C는 응용 프로그램에서만 대체하고 B는 인수에서만 대체한다.

콤비네이터의 현대적인 명칭은 1930년 하스켈 커리의 박사학위 논문에서 유래한다(B, C, K, W 시스템 참조). 쇤핀켈의 원본 논문에서는 지금 우리가 S, K, I, B, C라고 부르는 것을 각각 S, C, I, Z, T라고 불렀다.

의 섹션 3.2에서 제시된 바와 같이, 새로운 변환 규칙에서 비롯되는 결합기 크기 감소도 B와 C를 도입하지 않고도 달성할 수 있다. ^[8]

CL_K 대 CL_I 미적분

이 글에서 설명한 대로 CL과_K CL_I 미적분학을 구별해야 한다. 그 구별은 λ과_K λ_I 미적분 사이의 그것과 일치한다. λ_K 미적분과는 달리 calc_I 미적분은 추상적 착상을 다음과 같이 제한한다.

λx.E 여기서 x는 E에서 하나 이상의 자유 발생을 가진다.

따라서 결합기 K는 λ_I 미적분학이나 CL_I 미적분학에는 존재하지 않는다. CL의_I 상수는 I, B, C, S로 모든 CL_I 용어들이 구성될 수 있는 기초를 형성한다(모듈로 평등). 모든 λ항은_I λ항목을_K CL_K 콤비네이터로 변환하기 위해 위에서 제시한 규칙과 유사한 규칙에 따라 동등한_I CL 콤비네이터로 변환할 수 있다. 바렌트레트(1984)의 9장을 참조한다.

역변환

조합 용어에서 람다 용어로의 변환 L[ ]은 사소한 것이다.

L[I] = λx.x

L[K] = λx.λy.x

L[C] = λx.λy.λz.(x z y)

L[B] = λx.λy.λz.(x(y z))

L[S] = λx.λy.λz.(x z(y z))

L[(E₁ E₂)] = (L[E₁] L[E₂])

그러나 이러한 변환은 우리가 본 T[ ] 버전의 어떤 역변환도 아니라는 점에 유의하십시오.

결합 미적분의 불분해성

정상 형태는, 발생되는 원시 결합자가 있는 경우, 단순화할 수 있는 충분한 논거에 적용되지 않는 어떤 결합 용어다. 일반적인 결합 용어가 정상적인 형태를 가지고 있는지 여부, 두 결합 용어가 동등한지 여부 등은 불분명하다. 이것은 람다 용어에 대한 해당 문제의 불분명한 것과 같다. 그러나 직접적인 증거는 다음과 같다.

첫째, 용어

Ω = (S I I (S I I))

다음과 같이 3단계를 거치면 저절로 줄어들기 때문에 정상적인 형태가 없다.

(S I I (S I I))

= (I (S I I) (I (S I)))

= (S I I (I (S I)))

= (S I I (S I I))

그리고 분명히 다른 감소 순서는 표현을 짧게 할 수 없다.

자, N이 다음과 같은 정상적인 형태를 감지하는 결합체라고 가정합시다.

${\displaystyle(\mathbf {N} \x)={\begin{case}\mathbf {T},{\text{}}}}}}}}*x{\x{\text{}}}}}}*x{\mathbf {F},{\text{nother}.}}}\end{case}}$

(여기서 T와 F는 참과 거짓, conventionalx.λy.x와 λx.λy.y의 전통적인 교회 인코딩을 나타내며, 결합 논리로 변형된다. 결합 버전에는 T = K, F = (K I)가 있다.

자, 자자

Z = (C (B N (S I) Ω) I) I)

이제 (S I I Z)라는 용어를 고려하십시오. (S I I Z)의 형태가 정상인가? 다음과 같은 경우에도 그러하다.

(S I I Z)

= (I Z(I Z))

= (Z(I Z))

= (Z Z)

= (C (B N (S I) Ω) I Z) (Z의 정의)

= (C (B N (S I)) Ω Z I)

= (B N (S I) Z Ω I)

= (N (S I I Z) Ω I)

이제 (S I I Z)에 N을 적용해야 한다. (S I I Z)가 정상적인 형태를 갖거나 그렇지 않다. 만약 그것이 정상적인 형태를 가지고 있다면, 전술한 것은 다음과 같이 감소한다.

(N (S I I Z) Ω I)

= (K Ω I)(N의 정의)

= Ω

하지만 Ω은 정상적인 형태를 가지고 있지 않기 때문에 우리는 모순을 가지고 있다. 그러나 (S I I Z)에 정상적인 형태가 없다면, 전술한 것은 다음과 같이 감소한다.

(N (S I I Z) Ω I)

= (K I Ω I)(N의 정의)

= (I I)

= I

즉 (S I I Z)의 정상적인 형태는 단순히 I, 또 다른 모순이라는 뜻이다. 따라서 가상의 정상형식 콤비네이터 N은 존재할 수 없다.

라이스 정리의 결합 논리 아날로그는 완전한 비경쟁적 술어가 없다고 말한다. 술어는 적용하면 T 또는 F 중 하나를 반환하는 결합기이다. N이라는 술어는 N A = T 및 N B = F와 같은 두 개의 인수 A와 B가 있으면 비교가 되지 않는다. NM이 모든 인수 M에 대해 정상적인 형식을 가지고 있는 경우에만 결합기 N이 완성된다. 라이스 정리의 아날로그는 모든 완전한 술어는 사소한 것이라고 말한다. 이 정리의 증거는 다소 간단하다.

증명: by remedctio ad urlum. 완전한 비사소한 술어가 있다고 가정하자, N이라고 하자. N은 비사소한 술어가 되어야 하기 때문에, 다음과 같은 조합자 A와 B가 있다.

(N A) = T 및

(N B) = F.

NEGNATION ≡ λx. (만약 (N x) 다음에 B 다른 A) ≡ ≡x. (N x) B A를 정의한다.

SOLUEUM ≡ (Y NEGNation) 정의

고정된 포인트 정리가 주는 것은 다음과 같다: (NEGINALUM = (NEGINATION SOLUM),

부조리움 ≡ (Y 부정) = (NEGNATION (Y NEGNATION) ≡ (NEGNATION) ≡ (NEGNATION LUXYUM)

N은 다음 중 하나를 완료해야 하기 때문이다.

1. (N SOLUEUM) = F 또는
2. (N SOLUEUM) = T

• 사례 1: F = (N SOLUEUM) = N (NEGATION SOLUM) = (N A) = T, 모순.
• 사례 2: T = (N SOLUEUM) = N (NEGATION SOLUM) = (N B) = F, 다시 한번 모순.

따라서 (N SOLUM)은 T도 F도 아니며, 이는 N이 완전한 비사소한 술어가 될 것이라는 전제와는 상반되는 것이다. Q.E.D.

이 불해성 정리로부터 그것은 즉시 정상적인 형태를 가진 항과 정상적인 형태를 가지지 않은 항을 구별할 수 있는 완전한 술어가 없다는 것을 따른다. 또한 다음과 같이 EQUE라고 하는 완전한 술어가 없다는 것을 따른다.

(EQUAL A B) = A = B인 경우 T

(EQual A B) = A가 if B인 경우 F.

EQUE가 존재한다면, 모든 A, λx. (EQUAL x A)는 완전한 비사소한 술어일 것이다.

적용들

기능 언어의 컴파일

David Turner는 SASL 프로그래밍 언어를 구현하기 위해 결합기를 사용했다.

케네스 E. 아이버슨은 APL의 후속작인 J프로그래밍 언어에서 커리의 콤비네이터를 바탕으로 한 원시적 요소를 사용했다. 이를 통해 아이버슨은 암묵적 프로그래밍, 즉 변수가 없는 기능적 표현으로 프로그래밍할 수 있었고, 그와 같은 프로그램으로 작업할 수 있는 강력한 도구도 사용할 수 있었다. 사용자 정의 연산자라면 어떤 APL 같은 언어에서도 암묵적 프로그래밍이 가능한 것으로 나타났다.^[9]

논리학

Curry-Howard 이소모르퍼시즘은 논리학과 프로그래밍의 연관성을 내포하고 있다: 직관적 논리의 정리에 대한 모든 증거는 활자화된 람다 용어의 감소에 대응하고 반대로도 마찬가지다. 더욱이, 정리들은 함수형 서명으로 식별할 수 있다. 구체적으로 말하면, 형식화된 결합 논리는 증명 이론에서 힐버트 시스템에 해당한다.

K와 S 콤비네이터는 공리에 해당한다.

AK: A → (B → A),

AS: (A → (B → C) → (A → B) → (A → B), (A → C),

기능 적용은 분리(모더스 폰) 규칙에 해당된다.

MP: A와 A → B에서 유추한다.

AK, AS, MP로 구성된 미적분은 다음과 같이 볼 수 있는 직관적 논리의 관계적 파편에 대해 완성되어 있다. 연역적으로 닫힌 모든 공식의 집합 W를 포함 순서에 따라 고려하십시오. 그러면 $⟨{\displaystyle }$ ${\displaystyle W}$, ${\displaystyle \subseteq }$ {$\$ {\$displaystyle$ \$langle$W,\$subseteq \angle }}$은 직관적인 크립케 프레임으로$$, 우리는 이 프레임에$$ 모델 $⊩{\displaystyle }$ ${\displaystyle \Vdash }$을(를) 정의한다.

$X에서 A\iff A\in X.}$

This definition obeys the conditions on satisfaction of →: on one hand, if ${\displaystyle X\Vdash A\to B}$, and ${\displaystyle Y\in W}$ is such that ${\displaystyle Y\supseteq X}$ and ${\displaystyle Y\Vdash A}$, then ${\displaystyle Y\Vdash B}$ by modus ponens. On the other hand, if ${\displaystyle X\not \Vdash A\to B}$, then ${\displaystyle X,A\not \vdash B}$ by the deduction theorem, thus the deductive closure of ${\displaystyle X\cup \{A\}}$ is an element ${\displaystyle Y\in W}$ such that ${\displaystyle Y\supseteq X}$, ${\displaystyle Y⊩A}$$(\displaystyle Y\Vdash A}$및 $Y{\displaystyle }$ ${\displaystyle ⊮}$ ${\displaystyle B}$ ${\displaystyle$ Y$\not \Vdash B$

A는 미적분학에서 증명할 수 없는 어떤 공식이 되게 하라. 그러면 A는 빈 세트의 연역 폐쇄 X에 속하지 않으므로 ${\displaystyle X}$ ${\displaystyle ⊮}$ A ${\displaystyle X\not \Vdash A},$A는 직관적으로 유효하지 않다.

참고 항목

• 응용 컴퓨팅 시스템
• B, C, K, W 시스템
• 범주형 추상 기계
• 콤비네이션 분류 문법
• 명시적 대체
• 고정점 결합기
• 그래프감소기
• 람다 미적분 및 원통형 대수, 정량화 모델링 및 변수 제거에 대한 기타 접근법
• 스키 콤비네이터 미적분학
• 슈퍼컴바이너
• 앵무새 조롱하기

참조

추가 읽기

• Barendregt, Hendrik Pieter (1984). The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. Volume 103. North Holland. ISBN 0-444-87508-5. {{cite book}}: volume= 추가 텍스트(도움말)
• Curry, Haskell B.; Feys, Robert (1958). Combinatory Logic. Vol. Vol. I. Amsterdam: North Holland. ISBN 0-7204-2208-6. {{cite book}}: volume= 추가 텍스트(도움말)
• Curry, Haskell B.; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6. {{cite book}}: volume= 추가 텍스트(도움말)
• Field, Anthony J.; Harrison, Peter G. (1998). Functional Programming. Addison-Wesley. ISBN 0-201-19249-7.
• Hindley, J. Roger; Meredith, David (1990), "Principal type-schemes and condensed detachment", Journal of Symbolic Logic, 55 (1): 90–105, doi:10.2307/2274956, JSTOR 2274956, MR 1043546
• Hindley, J. R.; Seldin, J. P. (2008). λ-calculus and Combinators: An Introduction. Cambridge University Press.
• Paulson, Lawrence C. (1995). Foundations of Functional Programming. University of Cambridge.
• Quine, W. V. (1960). "Variables explained away". Proceedings of the American Philosophical Society. 104 (3): 343–347. JSTOR 985250. Quine 선정 논리 논문 23장(1966), 페이지 227–235로 재인쇄
• 쇤핀켈, 모세, 1924년, "위버 다이 바우스테인 데라메티스첸 로지크"는 From Frege에서 괴델까지 "수학적 논리학의 구성 요소들에 대하여"로 번역되었다: 1879–1931, 장 반 헤이제노르트, 에드. 하버드 대학 출판부, 1967. ISBN 0-674-32449-8 전투적 논리를 세운 기사.
• 스물리안, 레이먼드 1985년 앵무새 흉내내기. Knopf. ISBN 0-394-53491-3. 전투적 논리에 대한 완만한 소개로, 새를 관찰하는 은유법을 이용한 일련의 오락적 퍼즐로 제시된다.
• ______, 1994. 대각화 및 자체 참조. 옥스퍼드 대학 출판부 17~20장은 고정점 결과에 특별히 중점을 두고 전투적 논리에 대한 보다 공식적인 도입이다.
• Sørensen, Morten Heine B. 및 Pawew Urzyzyn, 1999. Curry-Howard Isomorphism에 대한 강의. 1999년 코펜하겐 대학교와 바르샤바 대학교
• Wolfengagen, V. E. (2003). Combinatory logic in programming: Computations with objects through examples and exercises (2nd ed.). Moscow: "Center JurInfoR" Ltd. ISBN 5-89158-101-9.
• Wolfram, Stephen (2021). Combinators: A Centennial View. Wolfram Media. ISBN 978-1-57955-043-1. eISBN 978-1-57955-044-8 1920년 모세 쇤핀켈에 의해 소개된 지 100년 만에, 콤비네이터의 발전을 축하하는 행사.

외부 링크

• 스탠포드 철학 백과사전: 카탈린 빔보의 "합성 논리"
• 1920-1931년 커리의 블록 노트.
• 키넌, 데이비드 C. (2001) "앵무새 해부하기: 애니메이션 감소가 있는 람다 미적분을 위한 그래픽 표기법"
• 래스만, 크리스 "컴비네이터 버드" 스물리얀(1985)의 진수를 많이 증류한 테이블.
• 'n' 드롭 결합기를 끌어다 놓으십시오. (자바 애플릿)
• 이항 람다 미적분학 및 결합 논리학.
• 결합 논리 감소 웹 서버