용어 재 작성이 필요한 이유 연구해야하는 주된 이유가

나는 약간의 googleing을하고 조금 짧게 나왔다.

나는 과학자, 프로그래머, 용어 재 작성 및 / 또는 용어 그래프 재 작성을 연구해야하는 주된 이유가 무엇인지 궁금합니다.

내가 알 수있는 한, 그것은 기능적 프로그램과 (제국적인) 프로그램 제어에 대한 기본적인 추론에 도움이됩니다. 분명히 이것은 논리 학자와 건설적인 추상 대수학을 연구하는 사람들에게 큰 관심 주제입니다.

어떤 도움이라도 가장 감사하겠습니다!



답변

이것이 당신이 이미 알고있는 것보다 더 많은 것을 가져올 것이라고 확신하지 않습니다. 그러나 용어 재 작성에 대해 궁금해하는 이유를 이해하지 못할 수도 있습니다. 도움이됩니다.

아시다시피, 문법은 문자열 재 작성 시스템입니다. Chomsky 계층의 맨 위에는 재귀 적으로 열거 가능한 (RE) 언어를 정의하고 튜링 머신의 계산 능력을 갖는 0 유형의 문법이 있습니다.

따라서 시스템을 다시 작성하는 것은 일반적으로 알고리즘을 표현하는 데 많은 영향을 미칩니다.

일반적으로 문자열의 문제점은 의미를 문자열에 첨부 할 수있는 확실한 방법이 없다는 것입니다. 일종의 무정형 재 작성입니다.

사람들이 일반적으로 관심을 갖는 것은 구조와 속성을 가진 특정 도메인에서 알고리즘을 표현하는 것입니다. 이러한 영역은 종종 기본 (원자) 실체로 정의되며 등가 관계 등으로 표현되는 다양한 작업으로 닫힙니다. 이것을 대수라고합니다.

이러한 영역은 종종 추상적입니다. 그러나 요소에 대한 계산은 구체적인 표현으로 만 표현할 수 있습니다. 용어는 이러한 요소를 자연스럽게 표현한 것으로, 요소를 재귀 적으로 원자 요소로 적용하여 다른 요소에 대해 요소를 얻을 수있는 방법을 표현하기 때문에 이러한 요소를 자연스럽게 표현한 것입니다 (일반 속성은 항상 끝까지 내려갈 필요는 없습니다). 용어는 (문자열과 같이) 알고리즘을 표현하기 위해 조작 할 수있는 일종의 트리 구조 구문입니다. 그러나 용어의 연산자 피연산자 구조는 또한 동질성을 통해 일부 추상 영역에서 의미론에 의미를 연관시킬 수 있습니다.

위키피디아에 대한 공식적인 견해와이 주제에 관한 많은 텍스트를 보는 대신 프로그램을 고려하십시오. 프로그램의 편리한 구문 표현은 AST (Abstract Syntax Tree)라고합니다. 그러나 AST는 프로그램 개체를 나타내는 용어 일뿐입니다. Dentational semantics는 추상 도메인을 정의하고이 도메인의 값을 동형을 통해 AST (또는 AST 하위 트리)에 연결하는 방법입니다. AST 형식의 프로그램은 다시 쓰기 규칙을 적용하여 변환하거나 최적화 할 수 있습니다 (모든 최적화가 그런 식으로 수행 될 수 있거나 수행되어야한다고 주장하지는 않습니다).

다양한 목적을위한 대수 표현의 변환은 용어 재 작성으로 표현 될 수 있습니다. 예를 들어, 일부 표현의 단순화. 도함수의 계산과 같이 다양한 유형의 계산이 자연스럽게 용어 재 작성으로 표현 될 수 있습니다. 동일한 의미 론적 엔티티가 여러 구문 표현을 가질 수있는 경우, 용어 재 작성은 대수학에서 정식 형태를 정의하기 위해 사용되기도합니다.

이 주제에 대한 wikipedia 기사를 참조하십시오 .


답변

제 생각은 Term Rewriting이 매우 근본적이기 때문에 하드웨어와 관계없이 매우 낮은 수준의 방식으로 설명 할 수 있기 때문입니다.

용어 재 작성은 문법을 설명 할 수 있지만 1 차 논리 등과 같은 논리 시스템에 대한 역학을 제공합니다. 증명 및 공제는 용어 작성으로 작성 될 수 있습니다. 그런 다음 용어 재 작성을 대체하는 것이 실제로는 유일한 작업입니다. 여기서의 단순성은 논리를 설명하고 있기 때문에 귀중합니다. 따라서 논리를 복잡하게 사용하여 시스템을 설명 할 수는 없습니다 (설명하려는 시스템이므로).

그런 다음 람다 미적분학에 대해 논리 / 축적 시스템으로 이야기하는 데 필요한 메커니즘을 제공하여 매우 공식적이고 기본적인 계산 버전을 제공합니다.

튜링 머신은 유용하지만 기본 정의에는 세트, 함수 등의 개념이 필요합니다. 빌드 된 것으로 추정되는 수학이 훨씬 많습니다.

반면 Lambda 미적분학은 논리에 의해 정의되므로 집합 이론, 함수 등에 대한 정의 방식을 많이 사용하지 않고도 사용할 수 있습니다.

논리로 모델링 된 용어 재 작성은 기능적 프로그래밍에만 적용되는 것은 아닙니다. 하드웨어 나 소프트웨어를 공식적으로 검증 할 때는 항상 어떤 종류의 추론을 수행해야하며이 추론은 용어 재 작성으로 모델링 할 수 있습니다.


답변

매우 실용적인 이유 중 하나는 표면 구문 재 작성을 사용하여 프로그램의 코드를 용어 (추상 구문 트리)로 조작 할 수있게 해주는 도구 인 프로그램 변환 시스템을 구성하기 때문입니다 .

이 시스템의 한 예인 DMS 소프트웨어 리엔지니어링 툴킷 은 다양한 프로그램 분석 및 대규모 변환 작업에 사용되었습니다. DMS 가 다시 쓰기를 표현 하는 방법을 볼 수 있습니다 . 이러한 재 작성은 배후에서 작동하는 연관 정류 용어 재 작성 시스템에 의해 적용됩니다.


답변