의미 부호화

의미론적 인코딩은 공식 언어 사이의 번역이다.프로그래머들에게 가장 친숙한 형태의 인코딩은 프로그래밍 언어를 기계 코드나 바이트 코드로 컴파일하는 것이다.문서 형식 간 변환도 인코딩 형식이다.TeX 또는 LaTeX 문서를 PostScript에 컴파일하는 것 또한 일반적으로 인코딩 프로세스에 직면한다.OCaml의 Camlp4와 같은 일부 고급 프리프로세서는 프로그래밍 언어를 다른 언어로 인코딩하는 것도 포함한다.

형식적으로 언어 A를 언어 B로 인코딩하는 것은 A의 모든 용어를 B로 매핑하는 것이다.만약 A를 B로 만족스럽게 인코딩하는 것이 있다면, B는 적어도 A만큼 강력(또는 적어도 표현력)하다고 간주된다.

특성.

비공식적인 번역 개념은 A의 모든 요소를 B의 동일한 요소에 매핑하는 것과 같은 사소한 인코딩을 허용하기 때문에 언어의 표현성을 결정하는 데 도움이 되기에 충분하지 않다.따라서 "충분히 좋은" 인코딩의 정의를 결정할 필요가 있다.이 개념은 용도에 따라 다르다.

$[\cdot ]:A\longrightarrow B$ 으로 인코딩 $[\cdot ]:A\longrightarrow B$ [ $[\cdot ]:A\longrightarrow B$ $[\cdot ]:A\longrightarrow B$ : $[\cdot ]:A\longrightarrow B$ $[\cdot ]:A\longrightarrow B$ B ${\displaystyle [\cdot ]:$ $A\longrightarrow$ B $}$ 은(는) 많은 속성을 보존할 것으로 예상된다 $[\cdot ]:A\longrightarrow B$ .

구성의 보존

견실함: $op_{A}$ n-ary 연산자에 대해 $op_{A}$ $op_{A}$ A ${\$ $A}$ 의 $op_{A}$ A}, 다음과 같은 B의 $op_{B}$ $op_{B}$ p B ${\$ n-ary 연산자가 존재한다.; $\forall T_{A}^{1},T_{A}^{2},\dots,T_{A}^{n},[op_{A}(T_{A}^{1}},T_{A}^{2},\cdots ,T_{A}^{n}]=op_{B}([T_{A}^{1}),[T_{A}^{2}],\cdots ,[T_{A}^{n}])$
완전성: $op_{A}$ n-ary 연산자에 대해 $op_{A}$ $op_{A}$ A ${\$ $A}$ 의 $op_{A}$ A}, 다음과 같은 B의 $op_{B}$ $op_{B}$ p B ${\$ n-ary 연산자가 존재한다.; $\forall T_{B}^{1},T_{B}^{2},\dots ,T_{B}^{n},\exists T_{A}^{1},\dots ,T_{A}^{n},op_{B}(T_{B}^{1},\cdots ,T_{B}^{N})=[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n}}}$

(주: 저자가 알고 있는 한, 이 완전성의 기준은 결코 사용되지 않는다.)

구성품의 보존은 어떤 흥미로운 성질을 "파손"하지 않고 구성품을 별도로 또는 함께 검사할 수 있다는 것을 보증하는 경우에 유용하다.특히 컴필레이션의 경우 이러한 건전성은 컴필레이션의 경우 컴필레이션의 분리 편성을 진행할 가능성을 보장하는 반면 완전성은 디컴필레이션의 가능성을 보장한다.

감액보존

이것은 A언어와 B언어 모두에 대한 감소의 개념의 존재를 가정한다.일반적으로, 프로그래밍 언어의 경우, 축소는 프로그램의 실행을 모델링하는 관계다.

1단계 감소를 위해 $\longrightarrow$ for $\longrightarrow$ 을(를) 쓰고, 감소를 몇 단계까지 진행하면 $\longrightarrow ^{*}$ $⟶{\$ 을(를) 쓴다.

견실함: 모든 용어 $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ , $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ ${\$ $T_{A}^{2}}$ of language A, if $T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}$ then $[T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]$ .
완전성: For every term $T_{A}^{1}$ of language A and every terms $T_{B}^{2}$ of language B, if $[T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}$ then there exists some $T_{A}^{2}$ such that $T_{B}^{2}=[T_{A}^{2}]$ ${\displaystyle T_{B}^{2}=[$ $T_{A}^{2}]}$ .

이 보존은 두 언어가 같은 방식으로 행동하도록 보장한다.건전성은 가능한 모든 행동이 보존되도록 보장하고, 완전성은 인코딩에 의해 어떠한 행동도 추가되지 않도록 보장한다.특히 프로그래밍 언어의 편찬의 경우, 종합된 프로그램이 프로그래밍 언어의 높은 수준의 의미론에 따라 동작한다는 것을 함께 의미한다.

종료 보존

이것은 또한 A언어와 B언어 모두에 감소의 개념의 존재를 가정한다.

견실함: $T_{A}$ 의 용어 $T_{A}$ T A {\ $displaystyle$ T_ ${A}$ 에 대해 $T_{A}$ $T_{A}$ $T_{A}$ ${\$ 의 모든 축소가 수렴되는 $T_{A}$ 경우 $[T_{A}]$ [ $[T_{A}]$ $[T_{A}]$ $[T_{A}]$ 의 모든 축소가 수렴된다 $[T_{A}]$ .
완전성: $[T_{A}]$ T $[T_{A}]$ $[T_{A}]$ ${\displaystyle$ [ $[T_{A}]$ ${A}}}$ 의 모든 감소가 수렴되는 $[T_{A}]$ 경우, $[T_{A}]$ A {\ $displaystyle T_{A}$ 의 $T_{A}$ 모든 감소가 수렴되는 경우, T $T_{A}$ ${\$ 의 모든 감소가 수렴된다.

프로그래밍 언어의 편찬의 경우, 건전성은 편찬이 끝없는 루프나 끝없는 반복과 같은 비종료를 도입하지 않는다는 것을 보장한다.완전성 속성은 언어 B가 언어 A로 작성된 프로그램을 연구하거나 시험하는 데 사용될 때 유용하며, 가능한 경우 코드의 주요 부분을 추출한다: 이 연구나 시험이 프로그램이 B에서 종료된다는 것을 증명하면 A에서도 종료된다.

관찰 보존

이것은 A 언어와 B 언어 모두에 대한 관찰 개념의 존재를 가정한다.프로그래밍 언어에서 대표적인 관측 가능성은 순수한 계산에 반대하여 입력과 출력의 결과물이다.HTML과 같은 설명 언어에서, 일반적으로 관찰할 수 있는 것은 페이지 렌더링의 결과물이다.

견실함: 모든 관찰 가능한 $obs_{A}$ b $obs_{A}$ $obs_{A}$ ${\$ $A}}$ 의 $obs_{A}$ 경우, 관측 가능한 $obs_{B}$ $obs_{B}$ B ${\$ $B}$ 의 $obs_{B}$ 조건으로서, 관측 가능한 $T_{A}$ $obs_{A}$ b $obs_{A}$ A ${\$ $A}$ 의 모든 용어에 대해 B}{ $A$ $[T_{A}]$ [ $[T_{A}]$ A $[T_{A}]$ $[T_{A}]$ 은 $[T_{A}]$ (는) $obs_{B}$ b $obs_{B}$ ${\$ 을(를) 관측할 수 있다 $obs_{B}$
완전성: 모든 관찰 가능한 $obs_{A}$ b $obs_{A}$ $obs_{A}$ ${\$ $A}}$ 의 $obs_{A}$ 경우, 관측 가능한 $obs_{B}$ $obs_{B}$ B ${\$ $B}}}$ 의 경우 $obs_{B}$ $[T_{A}]$ 관찰 가능한 $obs_{B}$ $obs_{B}$ B ${\$ $[T_{A}]$ 가 있는 $[T_{A}]$ 모든 용어에 대해 [TA $}$ $B$ $T_{A}$ $T_{A}$ ${\$ 은 $T_{A}$ (는) $obs_{A}$ b s $obs_{A}$ {\ $displaystyle obs_{{$ A}을(를) 관측할 수 있다. $A$

시뮬레이션 보존

이는 A 언어와 B 언어 모두에 시뮬레이션 개념의 존재를 가정한다.프로그래밍 언어에서 프로그램은 모든 동일한 (관측 가능한) 작업과 일부 다른 작업을 수행할 수 있다면 다른 작업을 시뮬레이션한다.시뮬레이션은 일반적으로 컴파일 시간 최적화를 설명하기 위해 사용된다.

견실함: 모든 용어 $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ , $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ ${\$ $T_{A}^{2}}$ , if $T_{A}^{2}$ simulates $T_{A}^{1}$ then $[T_{A}^{2}]$ simulates $[T_{A}^{1}]$ .
완전성: 모든 용어 $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ , $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ $T_{A}^{1},T_{A}^{2}$ ${\$ $T_{A}^{2}}$ , if $[T_{A}^{2}]$ simulates $[T_{A}^{1}]$ then $T_{A}^{2}$ simulates $T_{A}^{1}$ .

시뮬레이션의 보존은 관찰의 보존보다 훨씬 강력한 특성이다.결국, 그것은 2등분 보존의 속성보다 약하다.이전 사례처럼 컴파일을 위해서는 건전성이 중요한 반면, 완전성은 성질을 시험하거나 증명하는 데 유용하다.

동등성 보존

이것은 A 언어와 B 언어 모두에 동등성의 개념이 존재한다고 가정한다.전형적으로 이것은 구조화된 데이터의 동일성에 대한 개념 또는 구조 일치성이나 구조 동등성과 같은 구문론적으로 다르지만 의미론적으로 동일한 프로그램의 개념일 수 있다.

견실함: if two terms $T_{A}^{1}$ and $T_{A}^{2}$ are equivalent in A, then $[T_{A}^{1}]$ and $[T_{A}^{2}]$ are equivalent in B.
완전성: if two terms $[T_{A}^{1}]$ and $[T_{A}^{2}]$ are equivalent in B, then $T_{A}^{1}$ and $T_{A}^{2}$ are equivalent in A.

유통보존

이것은 A언어와 B언어 모두에 분포의 개념의 존재를 가정한다.일반적으로, Acrient, JoCaml 또는 E로 작성된 분산 프로그램의 컴파일에서는, 여러 컴퓨터나 CPU 사이에 프로세스와 데이터의 분배를 의미한다.

견실함: if a term $T_{A}$ is the composition of two agents $T_{A}^{1}~ ~T_{A}^{2}$ then $[T_{A}]$ must be the composition of two agents $[T_{A}^{1}]~ ~[T_{A}^{2}]$ .
완전성: if a term $[T_{A}]$ is the composition of two agents $T_{B}^{1}~ ~T_{B}^{2}$ then $T_{B}$ must be the composition of two agents $T_{A}^{1}~ ~T_{A}^{2}$ such that $[T_{A}^{1}]=T_{B}^{1}$ ${\$ $T_$ }^{1 $},$ $[T_{A}^{2}]=T_{B}^{2}$ [ $[T_{A}^{2}]=T_{B}^{2}$ $[T_{A}^{2}]=T_{B}^{2}$ $[T_{A}^{2}]=T_{B}^{2}$ $[T_{A}^{2}]=T_{B}^{2}$ = $[T_{A}^{2}]=T_{B}^{2}$ $[T_{A}^{2}]=T_{B}^{2}$ 2 ${\$ $T_{B}^{2$