환원전략

재작성할 때, 축소전략이나 재작성전략은 주어진 축소관계와 양립할 수 있는 각 객체나 용어에 대해 재작성을 명기하는 관계다.^[1]일부 저자는 평가 전략을 언급하기 위해 이 용어를 사용한다.^[2][3]

정의들

Formally, for an abstract rewriting system ${\displaystyle (A,\to )}$, a reduction strategy ${\displaystyle \to _{S}}$ is a binary relation on ${\displaystyle A}$ with ${\displaystyle \to _{S}\subseteq {\overset {+}{\to }}}$ , where ${\displaystyle {\overset {+}{\to }}}$ is$\to {\displaystyle }$ ${\displaystyle \to }($반사적 폐쇄는 아님).$$^[1]또한 전략의 정상적인 형태는 원래 재작성 시스템의 정상적인 형태와 같아야 한다. 즉, $모든{\displaystyle }$ ${\displaystyle a}$에 대해${\displaystyle ,<img\; alt="a"\; aria-hidden="true"\; class="mwe-math-fallback-image-inline"\; src="https://wikimedia.org/api/rest\_v1/media/math/render/svg/ffd2487510aa438433a2579450ab2b3d557e5edc"\; style="vertical-align:\; -0.338ex;\; width:1.23ex;\; height:1.676ex;"\; papago-attr-id="32">}$ $f{\displaystyle }$ $\exists {\displaystyle \mathrm{}}$ ${\displaystyle {}^{}.}$ a. ${\displaystyle a{}_{}}$ ${\displaystyle a_{}}$. b. ${\displaystyle {}_{}{}^{}}$. a. b$.$ a.$xists b'$가 $있는$ b ${\$$displaystyle$$a.$$a\to _{S}b$^[4]

한 단계 축소 전략은${\displaystyle {}_{}}$→ ${\displaystyle S_{}}$ ${\displaystyle \subseteq \to }$ ${\displaystyle \to _{S}\subseteq \to$ 그렇지 않으면 여러 단계 전략이다.^[5]

결정론적 전략은${\displaystyle {}_{}}$→ ${\displaystyle S_{}}$ ${\$ $_{S}$가 부분적인 함수인$$ 경우, 즉${\displaystyle }$∈ ${\displaystyle A}$ ${\displaystyle$ a$\\$$in$ A$}$에 대해 최대 $b{\displaystyle }$ ${\displaystyle b$$}$이($가)$ 하나 있는 것이다$.$ ${\displaystyle {그렇지}_{}}$ 않으면 비결정론적 전략이다.^[5]

용어 재작성

용어 재작성 시스템에서 재작성 전략은 모든 축소 가능한 하위 용어(redex) 중에서 한 기간 내에 축소(계약)해야 하는 것을 명시한다.

용어 재작성을 위한 한 단계 전략에는 다음이 포함된다.^[5]

• 가장 왼쪽 가장자리: 각 단계에서 가장 안쪽의 가장 왼쪽의 리덱스가 수축되며, 가장 안쪽 리덱스는 리덱스를^[6] 포함하지 않는 리덱스가 된다.
• 가장 왼쪽 가장자리: 각 단계에서 가장 바깥쪽 가장 왼쪽의 리덱스가 수축되며, 여기서 가장 바깥쪽 리덱스는 어떤 리덱스에도^[6] 포함되지 않은 리덱스임
• 가장 오른쪽 가장 오른쪽 가장 오른쪽 가장 오른쪽 가장 오른쪽 가장자리:

다단계 전략에는 다음이 포함된다.^[5]

• 가장 병렬 처리: 가장 안쪽의 모든 리디렉스를 동시에 줄인다.이것은 리덱스가 쌍방향으로 분리되어 있기 때문에 잘 정의되어 있다.
• 가장 병렬 처리: 유사
• 총-크누스 감소(^[7]전체 대체 또는 클레인 감소라고도 함):^[5] 용어의 모든 리덱스는 동시에 감소함

병렬 외측 및 총-핵감소(Gross-Knuth)는 거의 모든 직교 용어 재작성 시스템에 대해 초정규화(hyperormalization)하고 있는데, 이는 이러한 전략이 연속적인 전략 적용 사이에 임의적인 감소를 수행(완전히 다수)하더라도, 그것이 존재한다면 결국 정상적인 형태에 도달할 것이라는 것을 의미한다.^[8]

스트래티지오는 프로그래밍 용어 재작성 전략을 위해 특별히 고안된 도메인별 언어다.^[9]

람다 미적분학

람다 미적분학의 맥락에서 정상 순서 감소는 위에서 주어진 의미에서 가장 왼쪽에서 가장 바깥쪽으로 감소하는 것을 말한다.^[10]정상적인 순서 감소는 용어의 형식이 정상이면 결국 정상 순서 감소에 도달한다는 의미에서 정상 순서 감소라는 명칭이 정상화된 것이다.이것을 표준화 정리라고 한다.^[11][12]

사전 주문 통과 개념과 유사하게 람다 용어를 문자 문자열로 간주할 때 가장 왼쪽의 리덱스는 가장 왼쪽의 시작 문자와 가장 왼쪽의 시작 문자를 가진 리덱스(readx)를 나타내기 위해 가장 왼쪽의 감소를 참조하는 데 사용된다.^[13][14]순서 내 횡단을 사용하여 "가장 왼쪽"을 정의할 때 개념은 구별된다.예를 들어$,{\displaystyle }$ 용어 ( ${\displaystyle x}$ x${\displaystyle }$. ${\displaystyle x}$ ${\displaystyle \mathrm{\Omega }}$)${\displaystyle }$( ${\displaystyle \lambda }$ y${\displaystyle }$. ${\displaystyle I}$)에서$${\$displaystyle$(\$lambda$ x$.x\Oomega )(\lambda y).$여기서 $\Omega {\displaystyle \mathrm{}}$, ${\displaystyle I}$ ${\displaystyle \Oomega ,I}$이(가) 정의된 I$)$는 순서 내 트래버설의 가장 왼쪽 redex는 $\Omega {\displaystyle \mathrm{}}${\$displaystyle \Oomega }$이고, 가장 왼쪽 끝의 redex는 전체 식입니다.^[15]

적용적용적 주문감소란 가장 왼쪽 안쪽의 감소를 말한다.^[10]정상적인 순서와 대조적으로, 용어의 형식이 정상인 경우에도 적용적용적 순서 감소가 종료되지 않을 수 있다.^[10]예를 들어 적용 오더 감소를 이용하여 다음과 같은 감산 순서가 가능하다.

그러나 정상 순서 축소를 사용하면 동일한 시작점이 빠르게 정상 형태로 감소한다.

완전 β 감소란 각 단계에서 모든 redex를 줄일 수 있는 비결정적 1단계 전략을 말한다.^[3]다카하시의 병렬 β-축소란 용어의 모든 redex를 동시에 감소시키는 전략이다.^[16]

약감소

람다 추상화 시 감소를 허용한다는 점에서 정상적이고 적용 가능한 주문 감소가 강하다.이와는 대조적으로, 약한 감소는 람다 추상화 하에서는 줄어들지 않는다.^[17]호별 감축은 람다 추상화 내부가 아닌 가장 바깥쪽 가장 바깥쪽 가장자리를 줄인 약한 감축 전략이고, 가치별 감축은 람다 추상화 내부가 아닌 가장 왼쪽 가장 안쪽 가장 안쪽 가장자리를 줄이는 약한 감축 전략이다.이러한 전략은 호별 및 호별 평가 전략을 반영하기 위해 고안되었다.^[18]실제로 적용 순서 축소는 원래 알골 60과 현대 프로그래밍 언어에서 발견되는 가치별 매개변수 전달 기법을 모델링하기 위해 도입되었다.약한 감소의 개념과 결합하면 결과적으로 발생하는 가치별 감소는 실로 충실한 근사치가 된다.^[19]

불행하게도 약감축은 합성이 되지 않고,^[17] 약평가체제에 위배되는 관계를 제시하기 때문에 람다 미적분학의 전통적인 감량 방정식은 무용지물이다.^[19]그러나, 특히 리덱스가 추상화에 의해 구속되는 변수를 수반하지 않는 경우, 추상화 하에서는 제한된 형태의 감소를 허용함으로써, 시스템이 융합될 수 있도록 연장할 수 있다.^[17]예를 들어,λx.(λy.x)z는 람다 추상화에 들어있기 때문에 약한 축소전략을 위해 정상적인 형태를 취하고 있다.그러나 redex.(λy.y)z라는 용어는 readx(λy.y)z가 x를 지칭하지 않기 때문에 확장된 약세축소전략 하에서 여전히 축소될 수 있다.^[20]

최적감소

최적의 감축은 일련의 감축이 존재하지 않는 람다 용어의 존재에 의해 동기가 부여되어 중복 작업을 하지 않아도 이를 감소시킨다.예를 들어 다음을 고려하십시오.

(λg. (gx.x))) (hh.(λf.(f(zz.z))))) (λw.(w(λy.y))))))))

중첩된 3개의 항, x=(((λg…… ) (λh.y)), y=(ff. ...) (λw.z)), z=λw.(w(λy.y))로 구성되어 있다.여기서 x와 y에 대해 가능한 β-저감을 두 개만 수행할 수 있다.외부 x 항을 줄이면 먼저 내부 y 항이 중복되어 각 사본은 축소되어야 하지만, 내부 y 항을 먼저 줄이면 그 주장 z가 중복되어 h와 w의 값이 알려졌을 때 작업이 중복되게 된다.^[a]

β-축소 수행은 대체된 redex에 대한 정보를 공유하지 못하기 때문에 엄밀한 의미에서 람다 미적분학의 최적축소는 감소 전략이 아니다.대신에 그것은 공유되어야 하는 작업에 대한 정확한 개념을 포착하는 주석으로 표시된 람다 미적분인 람다 미적분학에 대해 정의된다.^{[21]: 113–114}

라벨은 셀 수 없을 정도로 무한대의 원자 라벨 집합과 $b{\displaystyle }$ ${\displaystyle ab},$${\$ 그리고$$ ${\displaystyle \underset{}{\_}}$ ${\$의 라벨 밑줄을 잇는 ${\displaystyle \mathrm{연결}}$로 구성된다.라벨로 표시된 항은 각 하위 항에 라벨이 있는 람다 미적분 항이다.람다 용어의 표준 초기 라벨링은 각 하위 용어에 고유한 원자 라벨을 제공한다.^{[21]: 132} 라벨로 표시된 β 감소는 다음을 통해 제공된다.^[22]

where ${\displaystyle \cdot }$ concatenates labels, ${\displaystyle \beta \cdot T^{\alpha }=T^{\beta \alpha }}$, and substitution ${\displaystyle M[x\mapsto N]}$ is defined as follows (using the Barendregt convention):^[22]

그 시스템은 혼합된 것으로 증명될 수 있다.최적 감소는 패밀리에 의한 감소를 이용한 정상 순서 또는 최측근 감소로 정의된다. 즉, 기능 부품 라벨이 동일한 모든 리덱스의 병렬 감소가 그것이다.^[23]가족 축소 단계의 최적(최소) 횟수를 수행한다는 점에서 전략이 최적이다.^[24]

최적 감소를 위한 실제 알고리즘은 1974년 최적 감소를 처음 정의한 지 10년이 넘은 1989년에 처음 설명되었다.^[25][26]볼로냐 최적 고차수 기계(BOHM)는 상호작용 네트에 대한 기법의 확장을 시제품으로 구현한 것이다.^{[21]: 362 [27]}람다스코프는 상호 작용 그물을 이용하는 등 최적 감소를 보다 최근에 구현한 것이다.^[28][b]

니즈 축소 콜 바이 니즈 감소

니즈 감소에 의한 호 감소는 라벨이 약간 다른 람다 미적분학에 대해 동일한 라벨을 가진 리덱스의 병렬 감소를 사용하여 최좌측 최측근 감소를 최적으로 약한 것으로 정의될 수 있다.^[17]대체 정의는 베타 규칙을 다음 "필요한" 계산을 찾아 평가하고 결과를 모든 위치로 대체하는 연산으로 변경한다.이를 위해서는 구문적으로 인접하지 않은 항을 줄일 수 있도록 베타 규칙을 확장할 필요가 있다.^[29]호별, 호별, 호별 가치와 마찬가지로 호별 감소가 '호별' 또는 게으른 평가로 알려진 평가 전략의 행동을 모방하기 위해 고안되었다.

참고 항목

• 감량제
• 환원 의미론
• 툰크

메모들

참조

외부 링크

• 람다 미적분 감소 작업대