모겐센-스코트 인코딩

컴퓨터 과학에서 스콧 인코딩은 람다 미적분학에서 (재발적) 데이터 유형을 나타내는 방법이다.교회 인코딩도 비슷한 기능을 수행한다.데이터와 연산자는 람다 미적분학에 내장된 수학 구조를 형성한다.

Church 인코딩은 기본 데이터 유형의 표현에서 시작하여 그것으로부터 축적되는 반면, Scott 인코딩은 대수 데이터 유형을 구성하는 가장 간단한 방법에서 시작한다.

모겐센-스코트 인코딩은 메타프로그래밍에 인코딩을 적용하여 스콧 인코딩을 확장하고 약간 수정한다.이 인코딩은 데이터로서 람다 미적분 용어를 메타 프로그램에 의해 운용할 수 있도록 한다.

역사

Scott 인코딩은 Dana Scott에^[1] 의해 출판되지 않은 일련의 강의 노트에서 첫 번째로 나타난다. Dana Scott는 Combinatorial Logic,^[2] Volume II에서 인용된다.Michel Parigot은 Scott 인코딩된 숫자에 대해 재귀자를 논리적으로 해석하고 이를 숫자의 "Stack type" 표현이라고 ^[3]지칭하며 강하게 정상화시켰다.토벤 모겐센은 이후 람다 용어의 데이터 인코딩을 위해 스콧 인코딩을 확장했다.^[4]

토론

람다 미적분은 데이터를 아직 적용에 필요한 모든 파라미터를 가지고 있지 않은 함수에 파라미터로 저장할 수 있도록 한다.예를 들어,

${\displaystyle(\\data x_{1}\ldots x_{n}).\lambda c.c\ x_{1}\ldots x_{n}\v_{1}\v_{n}\ldots v_{n}\f}$

$x{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$… x ${\displaystyle n_{}}$ ${\$ 필드가 v$$ ${\displaystyle {1\mathrm{}}_{}}$… v{${\displaystyle n_{}}$ ${\$ 값으로 초기화된 경우 기록 또는 구조체로 생각할 수 있다$.$그런 다음 함수 f에 용어를 적용하여 이러한 값에 접근할 수 있다.이렇게 하면

${\displaystyle f\ v_{1}\ldots v_{n}}$

c는 Haskell과 같은 기능 언어에서 대수 데이터 형식의 생성자를 나타낼 수 있다.이제 각각 $A{\displaystyle {}_{}}$ ${\displaystyle i_{}}$ ${\$ 인수가$$ 있는 N개의 생성자가 있다고 가정해 보십시오.

${\displaystyle {\begin{array}{c}{c}{c}{\textConstructor}&{\text}}}}{{Result}\hline (\lambda x_{1}\ldots x_{{{{{{}}}}})A_{1}.\lambda c_{1}\ldots c_{{N}c_{1}\x_{1}\ldots x_{{1}.A_{1})\v_{1}\ldots v_{A_{1})&f_{1}{1}\ldots f_{{N}&f_{1}\v_{1}\ldots v_{A_{1}\}\(\lambda x_{1}\ldots x_{{{1}{{{1}}{{{{{{{{{{{{{{}}}}}})A_{2}}.\lambda c_{1}\ldots c_{{N}c_{2}\x_{1}\ldots x_{{}}A_{2}})\v_{1}\ldots v_{A_{2}})&f_{1}\ldots f_{{N}&f_{2}\ v_{1}\ldots v_{A_{2}}\\\\\vdots &\(\lambda x_{1}ldots)\({1}ldots)A_{N}}.\lambda c_{1}\ldots c_{{N}\x_{N}\{1}\ldots x_{{{N}}}A_{N})\v_{1}\ldots v_{A_{N}}}&f_{1}\ldots f_{{N}\v_{1}\ldots v_{A_{N}\end{array}}}}}}}}}}}$

각 생성자는 함수 매개 변수 ${\displaystyle {f\mathrm{}}_{}}$ 1${\displaystyle {}_{}}$… ${\displaystyle f_{}}$ ${\$와 다른 함수를 선택한다$.$이것은 생성자를 기반으로 프로세스 흐름의 분기를 제공한다.각 생성자는 서로 다른 경성(매개변수의 수)을 가질 수 있다.생성자가 매개 변수를 가지고 있지 않으면 생성자 집합은 열거형처럼 작용한다. 즉, 고정된 수의 값을 가진 유형이다.생성자가 매개변수를 갖는 경우 재귀 데이터 구조를 구성할 수 있다.

정의

${\displaystyle {생성자}_{}^{}}$ $c{\displaystyle {}_{}}$ ${\displaystyle i_{}}$ ${\$$i}\}_{i=1}^{N$ 생성자 c i {\displaystyle c_{$i}}$가 arity $A{\displaystyle {}_{}}$ ${\displaystyle i_{}}${\$displaystyle A_{i}}$를 갖는 ${\displaystyle {}_{}^{}}$ 유형으로${\displaystyle }$D를 두십시오$.$

스콧 부호화

데이터 유형 D의 생성자 $c{\displaystyle {}_{}}$ ${\displaystyle i_{}}$ ${\$의 Scott 인코딩은

${\displaystyle \lambda x_{1}\ldots x_{{}A_{i}}.\lambda c_{1}\ldots c_{{N}c_{i}\x_{1}\ldots x_{{}}A_{i}}}$

모겐센-스코트 인코딩

모겐센은 스콧 인코딩을 확장하여 어떤 비정형 람다 용어를 데이터로 인코딩한다.이를 통해 람다 미적분 메타 프로그램 내에서 람다 용어를 데이터로 나타낼 수 있다.메타 함수 mse는 람다 항을 람다 항의 해당 데이터 표현으로 변환한다.

${\displaystyle {\begin{aligned}\operatorname {mse} [x]&=\lambda a,b,c.a\ x\\\operatorname {mse} [M\ N]&=\lambda a,b,c.b\ \operatorname {mse} [M]\ \operatorname {mse} [N]\\\operatorname {mse} [\lambda x.M]&=\lambda a,b,c.c\(\lambda x.\operatorname {mse}[M]]\\end{aigned}}}}}}$

'람바 용어'는 다음과 같은 세 가지 경우를 가진 태그가 붙은 조합으로 표현된다.

• 생성자 a - 변수(경고 1, 재귀가 아님)
• 생성자 b - 함수 응용 프로그램(성격 2, 두 인수 모두 재귀),
• 생성자 c - 람다-압축(경고 1, 재귀).

예를 들어,

${\displaystyle {\displaystyle}{l}\msename {mse}[\data x.f\ (x\ x)]\\\\b,c.c\ (\bda x.\msename {mse}[f\ (x\ x)])\\\\b,c.c\ (\bda x.\b.\bda a,b,c.b\\bname {mse} [f]\\msename {x\x])\\\\b,c.c\ (\bda x.\b.c.b\(\bda a,b,c.a\f)\\\\bda name {mse}[x\x])\\\\b,c.c\ (\bda x.\b.c.b\(\bda a,b.a\f)\(\bda a,b,c.b\ \bname {mse}[x])\\\\b,c\ (\bda x.\b.c.b\(\bda a,b,c.a\f)\\\(\bda a,b,c.a\)\ (\bda a,b,c.a\)\ (\bda,b,c.a\x)))\end{array}}}$

교회 인코딩과 비교

스콧 부호화는 술꾼들을 위한 교회 부호화와 일치한다.쌍의^{[citation needed]} 교회 인코딩은$$의 $D$의 c i {\$displaystyle$ c_${i}$를 인코딩하여 임의의 데이터 유형으로 일반화할 수 있다.

${\displaystyle \lambda x_{1}\ldots x_{{}A_{i}}.\lambda c_{1}\ldots c_{N}c_{i}(x_{1}c_{1}}\ldots c_{N})\ldots (x_{{{N})A_{i}}c_{1}\ldots c_{N}}$

이걸 모겐슨 스콧 부호화랑 비교해서

${\displaystyle \lambda x_{1}\ldots x_{{}A_{i}}.\lambda c_{1}\ldots c_{{N}c_{i}x_{1}\ldots x_{{{{}}}}A_{i}}}$

이러한 일반화를 통해 각 생성자가 상수(매개변수 없음)이기 때문에 스콧과 처치 인코딩은 열거된 모든 데이터 유형(예: 부울 데이터 유형)에서 일치한다.

프로그래밍에 대해교회나 스콧 인코딩을 사용하는 실용성과 관련하여, 대칭 균형:[5]Church-encoded 숫자와는linear-time 전임자 작업보다 가진 게 더 좋는constant-time 더하기 연산을 지원하는;Scott-encoded 숫자와는 미스터리 한 것보다 가진 게 더 좋는 constant-time 전임자 운영을 지탱하고 있다.near시간 추가 작업.

유형 정의

Scott가 인코딩한 데이터와 운영과 마찬가지로, 교회에서 인코딩된 데이터와 그에 대한 운영은 시스템 F에서 타이핑할 수 있다.그러나 인코딩은 훨씬 더 복잡하다.^[6]

스콧 인코딩의 자연수 형식은 양성 재귀 형식이다.

$\displaystyle \mu X.\all R.R\to (X\to R)\to R}$

전체 재귀 유형은 시스템 F의 일부가 아니지만 양성 재귀 유형은 시스템 F에서 다음 인코딩을 통해 표현할 수 있다.

$\displaystyle \mu X:G[X]=\all X:((G[X]\to X)\to X)}$

이러한 2가지 사실을 결합하면 Scott 인코딩의 System F 타입이 된다.

$([\displaystyle \ forall X.(\all R))R\to (X\to R)\to R)\to X)}$

이는 Church 인코딩 유형과 대조될 수 있다.

$모든 X에 대해 \displaystyle.X\to(X\to X)\to X}$

Church 인코딩은 2차 타입이지만 Scott 인코딩은 4차!

참고 항목

• 교회 부호화
• 시스템 F
• 람다 큐브

메모들

참조

• 스텀프, A. (2009)직접 반사 메타 프로그래밍.고차 및 심볼 연산, 22, 115-144.
• 모겐센, T.T. II. (1992년).람다 미적분학의 효율적인 자기 해석.J. 펑트. 프로그램, 2,345-363