이사 문자열

수학에서 람다 미적분과 연산 영역에서 감독이나 감독 문자열은 한 용어의 자유 변수를 추적하기 위한 메커니즘이다.느슨하게 말하면, 그것들은 자유 변수에 대한 일종의 메모, 즉 대수 또는 람다 표현에서 자유 변수를 신속하게 찾기 위한 최적화 기법으로 이해될 수 있다.이사 문자열은 1982년 케나웨이와 슬립에 의해 도입되었고, 베타 감소의 계산 복잡성 비용을 이해하고 제어하기 위한 메커니즘으로 시노트, 페르난데스, 맥키에^[1] 의해 더욱 발전되었다.

동기

베타 감소에서 왼쪽 표현식의 값은 오른쪽 표현으로 정의한다.

${\$$E)y\equiv E[x:=y]\,}$ 또는$$${\displaystyle }$( ${\displaystyle \lambda }$ ${\displaystyle x}$. ${\displaystyle E}$) ${\displaystyle y}$ ${\displaystyle \equiv }$ ${\displaystyle E}$[ ${\displaystyle y}$/ ${\displaystyle x}$ ${\displaystyle ]}$ ${\displaystyle(\lambda x)$$E)y\equiv E[y/x]}($y로 모든 x를 E(body)로 교체)

이것은 개념적으로 간단한 연산이지만 단계의 계산적 복잡성은 비교가 되지 않을 수 있다: 순진한 알고리즘은 자유 변수 x의 모든 발생에 대해 표현 E를 스캔한다.그러한 알고리즘은 표현 E의 길이에 분명히 O(n)이다.따라서 표현에서 자유 변수의 발생을 어떻게든 추적하려는 동기가 부여된다.표현에서 발생할 수 있는 모든 자유 변수의 위치를 추적하려고 할 수 있지만, 저장 측면에서 비용이 많이 들 수 있다. 더 나아가, 그것은 실제로 필요하지 않은 세부 정보 수준을 제공한다.이사 문자열은 구성요소의 용어로 자유변수의 사용을 추적하여 계층적 방식으로 자유변수를 추적하는 것이 올바른 모델임을 시사한다.

정의

단순성을 위해 대수, 즉 자유 변수, 상수 및 연산자의 집합이 자유롭게 결합될 수 있는 것을 고려한다.t라는 용어가 형식을 취한다고 가정한다.

${\displaystyle t:=f(t_{1},t_{2},\reason,t_{n}}}$

여기서 f는 자유 변수가 없는 아리티 n의 함수이며 t ${\displaystyle i_{}}$ ${\$는 자유 변수를 포함할 수도 있고 포함하지 않을 수도 있는 용어다$$.V는 모든 항 집합에서 발생할 수 있는 모든 자유 변수 집합을 나타내도록 한다.감독은 그 때 지도다.

$\displaystyle \sigma _{t:V\to P(\lbrace 1,2,\dots,n\rbrace )}$

from the free variables to the power set ${\displaystyle P(X)}$ of the set ${\displaystyle X=\lbrace 1,2,\dots ,n\rbrace }$. The values taken by ${\displaystyle \sigma _{t}}$ are simply a list of the indices of the ${\displaystyle t_{i}}$ in which a given free variable occurs.Thus, for example, if a free variable ${\displaystyle x\in V}$ occurs in ${\displaystyle t_{3}}$ and ${\displaystyle t_{5}}$ but in no other terms, then one has ${\displaystyle \sigma _{t}(x)=\lbrace 3,5\rbrace }$.

따라서 모든 용어 T의 집합에 있는$$ 모든 용어 $t{\displaystyle }$ ${\displaystyle \in }$ T ${\displaystyle t\in T}$에 대해 함수 ${\displaystyle t_{}}$ t$${\$displaystyle$\${\displaystyle {sigma}_{}}$ $_{t$를 유지하며, t만을 사용하는 대신 쌍(t ,${\displaystyle ,}$ ${\displaystyle {}_{}}$ ) $displaystystyle (t,\sigma _{t})$과 함께 작업한다$.$따라서 t에서 자유 변수를 찾는 시간의 복잡성은 변수가 발생하는 용어의 목록을 유지하는 공간 복잡성에 대해 거래된다.

일반사례

비록 위의 정의가 대수학이라는 용어로 공식화되었지만, 일반적인 개념은 보다 일반적으로 적용되며, 특히 명시적 대체의 틀 안에서 결합 알헤브라와 람다 미적분학 모두에 대해 정의될 수 있다.

참고 항목

• 용어 재작성 시스템
• 명시적 대체
• 메모화

참조

• F.R. 시노."감독 문자열 재방문: 고차 재작성 시 자유변수의 효율적인 표현을 위한 일반적 접근법."논리와 계산 저널 15(2), 201-218페이지 2005.