대부분의 함수형 프로그래밍 언어에서는 '위에서 아래쪽, 왼쪽에서 오른쪽 방향으로' 패턴 매칭(pattern matching)을 한다는 전략에 따라, 모호한(ambiguous) 특성을 갖는 룰의 정의를 허용하고 있다. 이 방법은 함수형 프로그래머에게 디폴트 룰을 정의할 수 있게 하는 직관적인 편리함을 제공하지만, 한편으로 모호한 룰 때문에 함수형 언어의 의미는 불명확해 질 수 있다. 좀 더 구체적으로, 함수형 언어가 갖는 대표적인 특성인 등식 추론(equational reasoning) 원리의 적용을 불가능하게 할 수 있으며, 함수형 언어를 람다 계산법으로 변환하는 데 있어서도 정형적인 방법이 아닌 임시방편적인(ad hoc) 방법에 의존할 수밖에 없게 한다. 본 연구에서는 지연(lazy) 함수형 언어의 패턴 매칭의 의미를 순수 선언적 특성을 갖는 항 개서 시스템(Term Rewriting Systems)의 분리성(separability) 이론과 연관시키고, 분리성 이론에 따라 지연 함수형 언어가 람다 계산법으로 변환될 수 있음을 보인다.
대부분의 함수형 프로그래밍 언어에서는 '위에서 아래쪽, 왼쪽에서 오른쪽 방향으로' 패턴 매칭(pattern matching)을 한다는 전략에 따라, 모호한(ambiguous) 특성을 갖는 룰의 정의를 허용하고 있다. 이 방법은 함수형 프로그래머에게 디폴트 룰을 정의할 수 있게 하는 직관적인 편리함을 제공하지만, 한편으로 모호한 룰 때문에 함수형 언어의 의미는 불명확해 질 수 있다. 좀 더 구체적으로, 함수형 언어가 갖는 대표적인 특성인 등식 추론(equational reasoning) 원리의 적용을 불가능하게 할 수 있으며, 함수형 언어를 람다 계산법으로 변환하는 데 있어서도 정형적인 방법이 아닌 임시방편적인(ad hoc) 방법에 의존할 수밖에 없게 한다. 본 연구에서는 지연(lazy) 함수형 언어의 패턴 매칭의 의미를 순수 선언적 특성을 갖는 항 개서 시스템(Term Rewriting Systems)의 분리성(separability) 이론과 연관시키고, 분리성 이론에 따라 지연 함수형 언어가 람다 계산법으로 변환될 수 있음을 보인다.
Most functional programming languages allows programmers to write ambiguous rules, under the strategy that pattern-matching will be performed in a direction of 'from top to bottom' way. While providing programmers with convenience and intuitive understanding of defining default rules, such ambiguous...
Most functional programming languages allows programmers to write ambiguous rules, under the strategy that pattern-matching will be performed in a direction of 'from top to bottom' way. While providing programmers with convenience and intuitive understanding of defining default rules, such ambiguous rules may make the semantics of functional languages unclear. More specifically, it may fail to apply the equational reasoning, one of most significant advantage of functional programming, and may cause to obscure finding a formal way of translating functional languages into the ${\lambda}$-calculus; as a result, we only get an ad hoc translation. In this paper, we associate with separability of term rewriting systems, holding purely-declarative property, pattern-matching semantics of lazy functional languages. Separability can serve a formalism for translating lazy functional languages into the ${\lambda}$-calculus.
Most functional programming languages allows programmers to write ambiguous rules, under the strategy that pattern-matching will be performed in a direction of 'from top to bottom' way. While providing programmers with convenience and intuitive understanding of defining default rules, such ambiguous rules may make the semantics of functional languages unclear. More specifically, it may fail to apply the equational reasoning, one of most significant advantage of functional programming, and may cause to obscure finding a formal way of translating functional languages into the ${\lambda}$-calculus; as a result, we only get an ad hoc translation. In this paper, we associate with separability of term rewriting systems, holding purely-declarative property, pattern-matching semantics of lazy functional languages. Separability can serve a formalism for translating lazy functional languages into the ${\lambda}$-calculus.
* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.
문제 정의
T 변환에 있어서 유사변수들의 선택 및 그들을 치환 확장하는 데 있어서의 특징에 대해서 논의해 보자. F의 조건을 만족하는 룰 %에서 어떤 한 변수에 대한 유사변수 여부를 결정하는 것은 7%에서 그 변수가 위치 한곳의 위쪽-왼쪽(uppeiTeft)의 패턴만을 고려하였을 때, 모호성이 발생하는 가에 의해서 결정된다.
논의한다. 변환을 적용하는 함수형 프로그래밍 언어를 문법적으로 구체적으로 정의하기보다는 함수형 프로그램 언어의 일반적인 특징을 개략적으로 제시하기로 한다.
본 연구에서 논의되는 함수형 프로그램 언어 F의 특징에 대해서 소개한다. 여기서 F는 어떤 특정 언어라기보다는 언어의 스킴(scheme)으로서 다음과 같은 TRS 의 구문적 특징을 갖는다.
본 연구에서는 Hask이1과 같은 지연(也砂) 함수형 언어의 패턴 매칭 의미를 순수 선언적 특성을 갖는 TRS 의 분리성(sepamb此y) 이론과 연관시켜 설명한다. 이 연구의 결과는 지연 함수형 언어를 람다 계산법으로 변환하는 데 필요한 이론적 기반으로 이용될 수 있다.
본 연구에서는 패턴 매칭과 지연 계산법을 적용하는 구성자 시스템 구조의 함수형 언어를 TRS로 변환하여 그 특징을 파악하였다. 지연 함수형-언어는 분리성을 갖는 TRS로 변환될 수 있으며, 분리성의 원리에 따라 람다 계산법으로 번역될 수 있다.
본 연구에서의 논의는 독자들이 함수형 프로그래밍과 TRS 및 람다 계산법에 기본적 지식을 가지고 있음을 전제로 하고 있다. Haskell 프로그래밍에 구체적인 관심이 있는 독자는 [3], TRS에 대한 자세한 내용은 [4], 람다 계산법에 대해서는 [5〕를 참조하기 바란다.
가설 설정
증명. (i) 변환 了의 정의를 고려할 때 당연히 성립한다.
제안 방법
분리가능성은 [8]에 자세히 논의되어 있다. 함수형 언어는 구성자 시스템의 구조를 가지므로, 본 연구에서는 일반적인 분리가능 시스템 대신 구성자 형태의 분리 가능성 시스템에 한정하여 논의한다. 이 경우 다루기가 휠 싼 쉽고 강 순차성과의 연관성도 깊다.
이론/모형
. 지연 계산법 (lazy evaluation)을 적용한다.
성능/효과
증명. (1) F의 군더더기 없는 룰의 조건, 알고리즘 12 와 알고리즘 13에 따라 1(完)은 직교성을 갖는다.
(1) 함수형 언어 戶의 조건에 따라 정의된 한 함수의 룰 , 디에 대해서 师)은 OTRS이다.
(3) HR)는 분리성을 가지며, 정리 8에 의해서 聞) 은강 순차성을 갖는다. □
(3) 衣를 포함하는 정규형 t의 지수는 £의한 주소 u로서 다음 조건을 만족한다.
⑹에서 모든 OTRS (orthogonal TRS)의 정규형을 갖는 모든 텀은 최소한 하나 이상의 요구 레덱스를 갖는 다는 것이 증명되었다. 그러나 어떤 레덱스가 요구레덱스인지는 모든 계산을 마치고 그 과정을 뒤돌아보았을 때만 알 수 있으므로, 일반적으로 OTRS에서 레덱스의 요구성을 판단하는 것은 불가능하다.
후속연구
이 변환은 요구성의 원리를 보전하며, 잘 정립된 강 순차성의 이론을 적용할 수 있다' 이 두 변환은 지연 계산 함수형 언어의 의미를 람다 계산법으로 설명하는 이론적 근거를 제공하고 있다. 다른 측면에서 볼 때, 본 연구는 함수형 프로그래밍의 둥식 추론에서의 한계와 적용 범위를 명확히 파악하는 데 이용될 수 있다.
이 연구의 결과는 지연 함수형 언어를 람다 계산법으로 변환하는 데 필요한 이론적 기반으로 이용될 수 있다.
참고문헌 (12)
Richard Kennaway, The Specificity Rule for Lazy Pattern-Matching in Ambiguous Term Rewriting Systems. ESOP '90, Lecture Notes in Computer Science No. 432, Springer-Verlag, 1990
Simon L. Peyton Jones, The Implementation of Functional Programming Languages. Prentice-Hall, 1987
Simon Thompson, The Craft of Functional Programming, 2nd Edition. Addison-Wesley, 1999
J.W. Klop, Term rewriting systems. In Abramsky et al., editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992
H. Barendregt, The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1984
G. Huet and J.-J. Levy, Computations in Orthogonal Rewrite Systems I and II. In Lassez and Plotkin, eds., Computational Logic: Essay in Honor of Alan Robinson, MIT Press 1991. (Originally appeared as Technical Report 359, INRIA, 1979.)
G. Berry. Sequentialite de l'evaluation formelle des ${\lambda}-expressions,$ in Proc. 3-e Colloque International sur la Programmation, Paris, 1978
변석우, 분리가능 시스템의 지수 추이성과 변환. 정보과학회 논문지: 소프트웨어 및 응용, 제31권 제5호, 659-666쪽, 2004년 5월
S. Byun, J.R. Kennaway, and R. Sleep, Lambda- definable Term Rewriting Systems, Lecture Notes in Computer Science 1023, pp. 106-115, Springer- Verlag, 1996
C. Bohm, Alcune proprieta delle forme ${\beta}-{\eta}-normali$ nel ${\lambda}-K-calcolo.$ IAC Pubbl., 696:19, 1968
A. Laville, Lazy pattern matchingin the ML programming. INRIA report 663, 1987
Y. Toyama, S. Smesters M. van Eekelen, and R. Plasmeijer, The Functional Strategy and Transitive Term Rewriting Systems. In (eds. Sleep, Plasmeijer, and van Eekelen) Term Graph Rewriting, John Wiley and Sons Ltd. 1993
※ AI-Helper는 부적절한 답변을 할 수 있습니다.