고차 추상 구문

이 문서에는 일반적인 참조 목록이 포함되어 있지만 대응하는 충분한 인라인 인용이 없습니다. 좀 더 정밀한 인용문을 도입하여 이 기사의 개선에 협조해 주십시오. (2010년 8월) (이 템플릿메시지의 삭제 방법 및 삭제 타이밍에 대해 알아보기)

컴퓨터 과학에서 고차 추상 구문(HOAS)은 가변 바인더를 가진 언어의 추상 구문 트리를 표현하는 기술입니다.

1차 추상 구문과의 관계

추상적인 구문은 추상적인데, 그 이유는 추상적인 성질을 가진 특정한 구조를 가진 수학적 객체로 표현되기 때문입니다.예를 들어 컴파일러에서 일반적으로 사용되는 First-order Abstract Syntax(FOAS; 1차 추상 구문) 트리에서 트리 구조는 하위 표현 관계를 의미하며, 이는 프로그램을 모호하게 하기 위해 괄호가 필요하지 않음을 의미합니다(구체 구문에서는 그대로).HOAS는 변수와 바인딩 사이트 간의 관계라는 추가 구조를 제공합니다.FOAS 표현에서 변수는 일반적으로 식별자로 표현되며 바인딩 사이트와 사용 간의 관계는 동일한 식별자를 사용하여 나타납니다.HOAS에서는 변수 이름은 없습니다.변수를 사용할 때마다 바인딩 사이트를 직접 참조합니다.

이 기술이 유용한 이유는 여러 가지가 있습니다.첫째, 프로그램의 바인딩 구조를 명확하게 합니다.FOAS 표현에서 연산자 우선순위를 설명할 필요가 없듯이 HOAS 표현을 해석하기 위해 바인딩 규칙과 스코프의 규칙을 가까이에 둘 필요가 없습니다.둘째, 알파 등가 프로그램(바인드 변수의 이름으로만 확산)은 HOAS에서 동일한 표현을 가지므로 동등성 검사를 보다 효율적으로 수행할 수 있습니다.

실행

HOAS 구현에 사용할 수 있는 수학적 객체 중 하나는 변수를 에지를 통해 바인딩 부위와 연관짓는 그래프입니다.HOAS(컴파일러 등)를 구현하는 또 다른 일반적인 방법은 de Bruijn 인덱스를 사용하는 것입니다.

논리 프로그래밍에 사용

구문에서 직접 "-바인딩"을 지원한 최초의 프로그래밍 언어는 고차 논리 프로그래밍 언어 "프롤로그"^[1]였습니다.HOAS라는 용어를 도입한 문서에서는 이를 설명하기 위해 프롤로그 코드를 사용했습니다.불행히도 HOAS라는 용어를 논리 프로그래밍에서 기능 프로그래밍 설정으로 옮길 때, 그 용어는 표현식 위의 함수와 구문에서 바인딩을 식별하는 것을 의미합니다.이 후자의 설정에서는 HOAS는 다른 문제의식을 가지고 있습니다."트리 구문"이라는 용어는 논리 프로그래밍 ^[3][4]설정에서 사용 가능한 표현 스타일을 구체적으로 나타내기 위해 도입되었습니다.§ 프롤로그의 바인딩 처리는 세부적으로는 다르지만 다음 섹션에서 자세히 설명하는 논리 프레임워크에서의 처리와 유사합니다.

논리 프레임워크에서 사용

논리 프레임워크 영역에서 고차 추상 구문이라는 용어는 보통 메타 언어의 바인더를 사용하여 오브젝트 언어의 바인딩 구조를 인코딩하는 특정 표현을 참조하기 위해 사용됩니다.

예를 들어 논리 프레임워크 LF는 화살표(→) 타입의 θ-type을 가진다.예를 들어, 매우 원시적인 언어를 정형화하려는 경우, 정형화되지 않은 표현식, 내장된 변수 세트 및 let constructure(예:let <var> = <exp> in <exp'>)는 변수를 바인드할 수 있습니다.var분명히exp표현으로exp'Twelf 구문에서는 다음과 같이 할 수 있습니다.

 exp : 유형.  변화하다 : 유형.  v : 변화하다 -> exp.  허락하다 : 변화하다 -> exp -> exp -> exp. 

여기서,exp모든 표현의 유형입니다.var모든 기본 제공 변수의 유형(표시되지 않은 자연수로 표시될 수 있음).상수v캐스팅 함수로 작용하며 변수가 식이라는 사실을 목격합니다.마지막으로, 상수는let형식의 구성을 나타냅니다.let <var> = <exp> in <exp>: 변수, 표현식(변수에 의해 바인딩됨) 및 다른 표현식(변수가 바인딩됨)을 받아들입니다.

동일한 오브젝트 언어의 표준 HOAS 표현은 다음과 같습니다.

 exp : 유형.  허락하다 : exp -> (exp -> exp) -> exp. 

이 표현에서는 오브젝트레벨 변수는 명시적으로 표시되지 않습니다.상수let(바인드되어 있는) 표현식과 메타 레벨 함수를 취합니다.exp→exp(렛의 몸통).이 함수는 상위 부분입니다. 자유 변수가 있는 식은 적용 시 메타 수준 함수에 의해 채워지는 구멍이 있는 식으로 표현됩니다.구체적인 예로, 우리는 객체 수준 식을 구성할 것이다.

 허락하다 x = 1 + 2  에 x + 3 

(숫자 및 덧셈을 위한 자연 컨스트럭터 가정) 위의 HOAS 시그니처를 사용하여

 허락하다 (플러스 1 2) ([y] 플러스 y 3) 

어디에[y] e는 twelf의 함수 구문입니다.${\displaystyle y}$.$$e \ $displaystyle$\$lambda$y .$e$ $\}$ 。

이 특정 표현에는 위의 것 이상의 장점이 있습니다.즉, 메타 수준의 바인딩 개념을 재사용함으로써 부호화는 정의/증명 없이 유형 보존 대체 등의 속성을 즐길 수 있습니다.이와 같이 HOAS를 사용하면 부호화의 바인딩과 관련된 보일러 플레이트 코드의 양을 대폭 줄일 수 있습니다.

고차 추상 구문은 일반적으로 객체 언어 변수를 수학적 의미에서 변수로 이해할 수 있는 경우에만 적용됩니다(즉, 일부 도메인의 임의 구성원에 대한 대리).예를 들어 동적 스코프 변수가 수학적 변수와 같이 동작하지 않기 때문에 동적 스코프의 HOAS 인코딩에서 얻을 수 있는 이점은 없습니다.

「 」를 참조해 주세요.

• 일반화 대수 데이터형
• 파라메트릭 고차 추상 구문(PHOAS)

레퍼런스

추가 정보

• J. Despeyroux; A. Felty; A. Hirschowitz (1995). Higher-Order Abstract Syntax in Coq. Lecture Notes in Computer Science. Vol. 902. pp. 124–138. doi:10.1007/BFb0014049. ISBN 978-3-540-59048-4. Archived from the original on 2006-08-30.
• Martin Hofmann (1999). Semantical analysis of higher-order abstract syntax. 14th Annual IEEE Symposium on Logic in Computer Science. p. 204. ISBN 0-7695-0158-3.
• Eli Barzilay; Stuart Allen (2002). Reflecting Higher-Order Abstract Syntax in Nuprl (PDF). Theorem Proving in Higher-Order Logics 2002. pp. 23–32. ISBN 3-540-44039-9. Archived from the original (PDF) on 2006-10-11.
• Eli Barzilay (2006). A Self-Hosting Evaluator using HOAS (PDF). ICFP Workshop on Scheme and Functional Programming 2006.