스키 콤비네이터 미적분학

스키 결합기 미적분은 결합 논리 시스템과 계산 시스템이다.소프트웨어 작성에는 편리하지 않지만 컴퓨터 프로그래밍 언어라고 생각할 수 있다.그 대신 지극히 단순한 튜링완전언어이기 때문에 알고리즘의 수학적 이론에서 중요하다.그것은 정형화되지 않은 람다 미적분의 축소판과 비유할 수 있다.모세 쇤핀켈과^[1] 하스켈 커리에 의해 소개되었다.^[2]

람다 미적분학의 모든 작업은 추상화 제거를 통해 스키 미적분으로 인코딩할 수 있으며, 잎이 세 가지 기호 S, K 및 I(결합기라고 함) 중 하나인 이진 트리로서 인코딩할 수 있다.

표기법

비록 이 시스템에서 객체의 가장 공식적인 표현은 이진 트리를 필요로 하지만, 형식적 설정성 때문에 모든 하위 트리가 상위화된 경우 또는 오른쪽 측면의 하위 트리만 상위화된 상태에서 상위화된 표현으로 나타낼 수 있다.그래서 왼쪽 하위 트리가 나무 KS이고 오른쪽 하위 트리가 나무 SK인 나무는 (KS) (SK)로, 또는 더 간단히 KS(SK)로 입력되는데, 이는 (요식이나 가독성이 필요하기 때문에) 나무로 완전히 그려지는 것이 아니라 말이다.오른쪽 하위 트리만 괄호화하면 다음과 같은 표기법이 왼쪽 연관된다.ISK는 ((IS)K)를 의미한다.

비공식 설명

비공식적으로, 그리고 프로그래밍 언어 전문 용어를 사용하여 트리(xy)는 y 인수에 적용된 함수 x로 생각할 수 있다.평가할 때(즉, 함수를 인수에 "적용"하면 트리는 "값을 반환한다" 즉, 다른 트리로 변환한다.「기능」, 「주장」, 「가치」는 콤비네이터나 바이너리 트리 중 하나이다.만약 그것들이 2진수라면, 그들은 필요하다면 기능으로도 생각할 수 있다.

평가 운전은 다음과 같이 정의된다.

(x, y, z는 S, K, I 함수로 만든 표현식을 나타내며 값 설정):

나는 그것의 주장을 답한다:

Ix = x

K는 어떤 인수 x에 적용되었을 때 1개의 인수 상수 함수 Kx를 산출하며, 어떤 인수에도 적용되면 x를 반환한다.

Kxy = x

S는 대체 연산자다.세 가지 주장을 취하다가 세 번째에 적용된 첫 번째 주장을 반환하고, 그 다음 세 번째에 적용된 두 번째 논쟁의 결과에 적용된다.보다 명확하게 설명:

Sxyz = xz(yz)

계산 예: SKSK는 S-규칙으로 KK(SK)를 평가한다.KK(SK)를 평가하면 K-규칙으로 K를 받는다.더 이상의 규칙을 적용할 수 없기 때문에 계산은 여기서 중단된다.

모든 트리 x와 모든 트리 y에 대해 SKxy는 항상 Ky(xy) = y의 두 단계로 평가하므로 SKxy를 평가하는 최종 결과는 항상 y를 평가하는 결과와 동일할 것이다.우리는 skx와 내가 "기능적으로 동등하다"고 말한다. 왜냐하면 그들은 어떤 y에 적용해도 항상 같은 결과를 내기 때문이다.

이러한 정의에서 모든 표현에서 I의 발생은 (SKK) 또는 (SKS) 또는 (SK 무엇이든)로 대체될 수 있고 결과 표현에서도 동일한 결과를 산출할 수 있으므로, SKI 미적분은 람다 미적분의 계산을 완전히 수행할 수 있는 최소 시스템이 아님을 알 수 있다.그래서 "나"는 단지 통사당일 뿐이다.내가 선택적이기 때문에 이 시스템은 SK 미적분학 또는 SK 콤비네이터 미적분학으로도 불린다.

콤비네이터를 하나만 사용하여 완전한 시스템을 정의할 수 있다.크리스 바커의 iota 콤비네이터가 그 예로서 다음과 같이 S와 K의 용어로 표현할 수 있다.

ιx = xSK

iota 콤비네이터에서 S, K, I를 재구성할 수 있다.Applying ι to itself gives ιι = ιSK = SSKK = SK(KK) which is functionally equivalent to I. K can be constructed by applying ι twice to I (which is equivalent to application of ι to itself): ι(ι(ιι)) = ι(ιιSK) = ι(ISK) = ι(SK) = SKSK = K. Applying ι one more time gives ι(ι(ι(ιι))) = ιK = KSK = S.

형식 정의

또한 이 시스템의 용어와 파생어는 보다 공식적으로 정의될 수 있다.

용어: T 용어의 집합은 다음 규칙에 의해 재귀적으로 정의된다.

S, K, 그리고 나는 조건이다.
τ과₁ τ이₂ 용어라면 ( (τ₁₂)는 용어다.
처음 두 규칙에서 그렇게 할 필요가 없다면 그 어떤 것도 용어가 아니다.

파생어: 파생어(derivation)는 다음 규칙에 의해 재귀적으로 정의된 용어의 유한한 순서(여기서 α와 α는 알파벳 {S, K, I, (, )}을(를) 넘는 단어인 반면 β, Δ는 용어인 경우:

Δ가 α(Iβ)ι 형태의 표현으로 끝나는 파생이라면 Δ 다음에 αβι이라는 용어가 파생된 것이다.
Δ가 α((Kβ)γ)ι 형태의 표현으로 끝나는 파생어라면, Δ에 이어 αβι이라는 용어가 파생어다.
Δ가 α(((Sβ)))γ)) 형태의 표현으로 끝나는 파생이라면, Δ에 이어 α(βΔ)ι라는 용어가 파생된 것이다.

시퀀스가 시작하기에 유효한 파생이라고 가정하면, 이러한 규칙을 사용하여 확장할 수 있다.[1]

재귀 매개 변수 전달 및 인용

K=λq.λi.q.: q를 인용하고 i를 무시하다

S=x.xy.λz.(xz(yz): 매개변수가 루트에서 가지로 흐를 수 있고 ID에 의해 판독될 수 있는 이진 트리를 형성한다.펑크=((SK)K) 또는 인용된 람다 q를 사용하여 읽는다.

스키 표현식

자체 적용 및 재귀

SII는 다음과 같은 주장을 받아들여 그 주장을 자신에게 적용하는 표현이다.

SIIα = Iα(Iα) = αα

이것의 한 가지 흥미로운 특성은 SII(SII)라는 표현을 다시 설명할 수 없게 만든다는 것이다.

SII(SII) = I(SII)(I(SII) = I(SII) = SII(SII)

이것에서 비롯되는 또 다른 것은, 그것은 여러분이 어떤 것을 다른 것의 자기 적용에 적용하는 기능을 쓸 수 있게 한다는 것이다.

(S(Kα)(SII)β = Kαβ(SIIβ) = α(SIIβ) = α(β)

이 기능은 재귀에 사용할 수 있다.β가 다른 것의 자기응용에 α를 적용하는 함수라면, β를 자응하는 β는 β에 대해 α를 재귀적으로 수행한다.보다 명확하게, 다음과 같은 경우:

β = S(Kα)(SII)

(

β) = … {\

displaystyle \ldots }

반전표현

S(K(SI)K는 다음 두 용어를 반대로 한다.

S(K(SI)Kαβ →

K(SI)α(Kα)β →

SI(Kα)β →

Iβ(Kαβ) →

이βα →

βα

부울 논리학

또한 스키 결합기 미적분학은 if-ten-else 구조의 형태로 부울 논리를 구현할 수 있다.if-then-else 구조는 참(T) 또는 거짓(F)인 부울 식과 다음과 같은 두 개의 인수로 구성된다.

Txy = x

그리고

Fxy = y

핵심은 두 부울 식을 정의하는 것이다.첫 번째는 우리의 기본적인 결합자 중 하나와 같다.

T = K

Kxy = x

두 번째 방법은 매우 간단하다.

F = SK

SKxy = Ky(xy) = y

일단 참과 거짓이 정의되면, 모든 부울 논리는 if-ten-else 구조의 관점에서 구현될 수 있다.

Boolean NOT(주어진 Boolean과 반대되는 값을 반환하는)는 if-ten-ten-else 구조와 동일하게 작동하므로, F와 T를 두 번째와 세 번째 값으로 하여 사후 처리 작업으로 구현할 수 있다.

NOT = (F)(T) = (SK)(K)

만일 이것이 if-ten-else 구조로 되어 있다면, 이것은 예상된 결과를 가지고 있다는 것을 보여줄 수 있다.

(T)NOT = T(F)(T) = F

(F)NOT = F(F)(T) = T

Boolean OR (이를 둘러싼 두 부울 값 중 하나가 T인 경우 T를 반환하는 것)은 if-ten-else 구조와 동일하게 작동하므로, 다음 두 번째 값으로 If-ten-else 구조로 구현될 수 있다.

OR = T = K

if-ten-else 구조로 이 방법을 적용하면 다음과 같은 예상 결과를 얻을 수 있다.

(T)OR(T) = T(T) = T

(T)OR(F) = T(T)(F) = T

(F)OR(T) = F(T) = T

(F)OR(F) = F(T)(F) = F

부울 AND(두 부울 값이 모두 T일 경우 T를 반환함)는 F를 세 번째 값으로 하는 if-then-else 구조와 동일하게 작동하므로 사후 처리 작업으로 구현할 수 있다.

AND = F = SK

if-ten-else 구조로 이 방법을 적용하면 다음과 같은 예상 결과를 얻을 수 있다.

(T)(T)AND = T(T)(F) = T

(T)(F)AND = T(F) = F

(F)(T)AND = F(T)(F) = F

(F)(F)AND = F(F) = F(F) = F

이는 SKI 표기법에서 T, F, NOT(후처리 운영자), OR(인픽스 운영자) 및 AND(후처리 운영자)를 정의하기 때문에, 이는 SKI 시스템이 부울 논리를 완전히 표현할 수 있음을 증명한다.

스키 미적분이 완성되면 NOT, OR 및 AND를 접두사 연산자로 표현할 수도 있다.

NOT = S(SI(KF))(KT)(S(SI(KF))(KT)x = SI(KF)x(KTX) = Ix(KFX)T = xFT)

OR = SI(KT) (SI(KT)xy = Ix(KTX)y = xTy)

AND = SS(K(KF))(SS(KF))xy = Sx(KF)xy = XY(KFY) = xYF)

직감적 논리에 대한 연결

결합자 K와 S는 두 가지 잘 알려진 송신 논리 공리에 해당한다.

AK : A \to (B \to A)

,

AS :

(

A \to

(

B

→ C

) \to

(

A

→

B)

→ (A → B) →

(A

→

C)).

함수 적용은 규칙 모드에 해당된다.

MP

:

A

와 A →

B

로부터,

유추

B.

공리는 AK와 AS로 되어 있고, 규칙 MP는 직관 논리의 관계적인 파편에 대해 완성되어 있다.결합 논리를 모델로 삼으려면:

고전적 논리의 관계적 단편은 배제된 중간 법칙, 즉 피어의 법칙과 결합적 유사성을 필요로 할 것이다.
완전한 고전적 논리에서는 전위 공리 $F$ → $A$ 에 대한 결합적 유사성이 필요하다.

결합자의 유형과 그에 상응하는 논리 공리 사이의 이러한 연결은 Curry-Howard 이형성의 한 예다.

감소의 예

${\textrm {SKI(KIS)}\오른쪽 화살표 {\textrm {SKII}}\오른쪽 화살표 {\textrum {KI(II)}}\오른쪽 화살표 {\textrum {KII}}\오른쪽 화살표 {\textrum{I}$
${\textrm {KS(I(SKSI))}\오른쪽 화살표 {\textrm {KS(I(SI))}}\오른쪽 화살표 {\textrm {KS(KI)}}}\오른쪽 화살표 {\textrum {KS(II)}\오른쪽 화살표 {\textrum {KSI}\오른쪽 화살표 {\textrum {S}$
${\textrm {SKIK}\오른쪽 화살표 {\textrum {KK}}\오른쪽 화살표 {\textrum {KK}}\오른쪽 화살표 {\textrum {K}}$

참고 항목

결합 논리학
B, C, K, W 시스템
고정점 결합기
람다 미적분학
기능 프로그래밍
언람바 프로그래밍 언어
Iota와 Jot 프로그래밍 언어는 스키보다 훨씬 단순하도록 설계되었다.
앵무새 조롱하기

참조

^ 1924. "Vausteine deramaturischen Logik", Matheatische Annalen 92, 페이지 305–316.Stefan Bauer-Mengelberg가 Jean van Heijenoort, 1967년에 "수학적 논리학의 구성 요소 위에서"로 번역했다.수학논리의 출처, 1879-1931.하버드 유니브프레스: 355-66.
^ Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [Foundations of combinatorial logic]. American Journal of Mathematics (in German). The Johns Hopkins University Press. 52 (3): 509–536. doi:10.2307/2370619. JSTOR 2370619.

Smullyan, Raymond (1985). To Mock a Mockingbird. Knopf. ISBN 0-394-53491-3. 전투적 논리에 대한 완만한 소개로, 새를 관찰하는 은유법을 이용한 일련의 오락적 퍼즐로 제시된다.
— (1994). "Ch. 17–20". Diagonalization and Self-Reference. Oxford University Press. ISBN 9780198534501. OCLC 473553893. 고정점 결과에 특별히 중점을 두고 전투적 논리에 대한 보다 공식적인 도입이다.

외부 링크

O'Donnell, Mike "The SKI Combinator Miculus as a Universal System."
키넌, 데이비드 C.(2001) "앵무새 해부하기"
래스만, 크리스 "컴비네이터 버드"
"'n' 드롭 콤비네이터(Java 애플릿) 드랙'."
Malculus of Mobile Processs, Part I (PostScript) (Milner, Parrow 및 Walker)은 25-28페이지의 SKI 미적분학에 대한 콤비네이터 그래프 감소 계획을 보여준다.
녹 프로그래밍 언어는 전통적인 어셈블리 언어가 튜링머신을 기반으로 하는 것과 같은 방식으로 SK 콤비네이터 미적분학을 기반으로 한 어셈블리 언어로 볼 수 있다.Nock 명령 2("Nock 연산자")는 S 콤비네이터, Nock 명령 1은 K 콤비네이터다.노크에 있는 다른 원시적 지침(지침 0,3,4,5와 사이비지침 '불확실성 단서')은 보편적 연산에는 필요하지 않지만, 2진수 데이터 구조와 산술 처리를 위한 시설을 제공함으로써 프로그래밍을 더욱 편리하게 하고, 노크는 또한 b일 수도 있었던 5가지 지침(6,7,8,9,10)을 더 제공한다.이 원시적인 것에서 벗어났지

[1] 1924. "Vausteine deramaturischen Logik", Matheatische Annalen 92, 페이지 305–316.Stefan Bauer-Mengelberg가 Jean van Heijenoort, 1967년에 "수학적 논리학의 구성 요소 위에서"로 번역했다.수학논리의 출처, 1879-1931.하버드 유니브프레스: 355-66.

[2] Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [Foundations of combinatorial logic]. American Journal of Mathematics (in German). The Johns Hopkins University Press. 52 (3): 509–536. doi:10.2307/2370619. JSTOR 2370619.

[1]

[2]

Search