함수형 언어의 평가와 선택

함수형 언어(Functional Language)의 핵심 함수형 언어가 점점 많은 매체에 노출되고,더 많은 언어들이 함수형 언어의 특징을 하나 둘받아들이고 있다. 함수형 언어, 적어도 그 특징이점점 대세가 되고 있다는 이야기이다. 하지만,함수형 언어가 대체 무엇이란 말인가?무엇인지도 모르는 것이 대세가 된다고 할 수는 없지않은가? 함수형 언어란 아주 단순히 말해서 함수가표현식[1]인 언어를 말한다. 다른 말로는 함수가값이기 때문에 다른 함수를 호출해서 함수를얻어내거나 함수의 인자로 함수를 넘길 수 있는언어를 말한다. 그렇다면 이 단순화된 핵심만을포함하는 언어로 함수형 언어의 핵심을 이해할 수있지 않을까? 이게 바로 람다 대수(Lambda Calculus)의역할이다.[2] 람다 대수는 딱 세 종류의 표현식만을 가지고 있다.변수 (xx, yy, …\ldots)매개변수 xx에 인자를 받아 한 표현식 MM(함수의 몸체)을계산하는 함수 (λx→M\lambda x\to M)어떤 표현식 LL의 결과 함수를 인자 NN으로 호출 (L NL\ N)<이후의 설명에서는 MM 과 NN, 그리고 LL이라는 이름을임의의 표현식을 나타내기 위해 사용할 것이다.람다 대수가 어떤 것들을 표현할 수 있는가? 앞에서 말했듯이람다 대수는 함수의 인자와 함수 호출의 결과가 모두함수인 표현식을 포함한다. 예를 들어λx→(λy→y)\lambda x \to (\lambda y \to y) 는 매개변수 xx에 인자를받아 함수 λy→y\lambda y \to y를 되돌려주는 함수이고,λx→(x (λy→y))\lambda x \to (x\ (\lambda y \to y))는 매개변수 xx에함수인 인자를 받아 그 함수를 (λy→y\lambda y \to y를 인자로사용하여) 호출하는 함수이다.람다 대수(Lambda Calculus)의 평가(Evaluation) 이제 문제는<그래서 람다 대수의 표현식이 하는 일이 뭔데?<이다. 위의 표현식에 대한 소개는 산수로 말하자면x+yx + y와 같이 연산자(++)와 연산항(xx와 yy)로부터얻어지는 문법만을 설명하고 있고, 3+53 + 5와 같은구체적인 표현식을 계산해서 88이라는 결과 값을 내놓는방식을 설명하고 있지 않다. 이런 표현식으로부터 값을얻어내는 것을 언어의"평가 절차"("Evaluation Procedure")라고 한다.람다 대수의 평가 절차를 설명하는 것은 어렵지 않다. 적어도표면적으로는 말이다.함수는 이미 값이다.함수 λx→M\lambda x \to M을 NN으로 호출하면 MM에등장하는 모든 xx을 NN으로 치환(Substitute)하고결과 표현식의 평가를 계속한다.<이는 겉으로 보기에는 말이 되는 설명처럼 보인다. 하지만 이 설명을실제로 해석기(Interpreter)로 구현하려고 시도한다면 이 설명이사실 여러 세부사항을 무시하고 있다는 점을 깨닫게 될 것이다.함수 호출 L NL\ N에서 LL이 (아직) λx→M′\lambda x \to M'꼴이 아닐 때는 어떻게 해야하지?함수 호출 (λx→M) N(\lambda x \to M)\ N에서 NN을 먼저평가하는 게 낫지 않나? xx가 MM에 여러번 등장한다면NN을 여러번 평가해야 할텐데?<첫번째 문제는 비교적 간단히 해결할 수 있다. LL을 먼저 평가해서λx→M′\lambda x \to M' 꼴의 결과 값을 얻어낸 뒤에 호출을실행하면 되기 때문이다. 반면에 두번째 질문은 좀 더 미묘한 문제를가지고 있다. 함수 호출의 평가에서 발생하는 이 문제에 구체적인답을 하기 위해서는 값에 의한 호출(Call-By-Value, CBV)와이름에 의한 호출(Call-By-Name, CBN)이 무엇인지 이해해야 한다.값에 의한 호출(Call-By-Value)? 이름에 의한 호출(Call-By-Name)? 앞에서 말한 함수 호출에서부터 발생하는 문제는 사실함수형 언어에서만 발생하는 문제는 아니다. C와 같은명령형 언어에서도 함수를 호출할 때 인자를 먼저평가해야하는지를 결정해야하기 때문이다. 즉 이 문제는함수를 가지고 있고 함수를 호출해야하는 모든 언어들이가지고 있는 문제이다. 그렇다면 이 일반적인 문제를 어떻게 해결하는가? 대부분의 언어가취하는 가장 대표적인 방식은 "값에 의한호출"("Call-By-Value", "CBV")이라고 한다. 이 함수 호출평가 절차에서는 함수의 몸체에 인자를 치환하기 전에[3] 인자를먼저 평가한다. 이 방식을 사용하면 인자를 여러번 평가해야하는상황을 피할 수 있다. 또 다른 방식은 "이름에 의한 호출"("Call-By-Name","CBN")이라고 한다. 이 방식에서는 함수의 몸체에 인자를 우선치환한 후 몸체를 평가한다. 몇몇 언어의 매크로(Macro)와 같은기능이 이 방식을 사용한다. 얼핏 보기에는 CBN은 장점이 없어보인다.그러나 함수가 인자를 사용하지 않을 경우는 CBN이 장점을 가진다는 것을볼 수 있다. 극단적으로 평가가 종료되지 않는표현식(Non-terminating expression)이 있다면[4] CBV는종료하지 않고 CBN만이 종료하는 경우가 있음을 다음 예시를 통해 살펴보자.표현식 (λx→(λy→y)) N(\lambda x \to (\lambda y \to y))\ N이 있다고 할 때,NN이 평가가 종료되지 않는 표현식이라고 하. 이 경우 CBV를 따른다면종료하지 않는 NN 평가를 먼저 수행하느라 이 표현식의 값을 얻어낼 수없지만, CBN을 따른다면 λy→y\lambda y \to y라는 값을 손쉽게 얻어낼수 있다. 바로 이런 상황 때문에<CBN은 CBV보다 일반적으로 더 많은 표현식들을 평가할 수 있다<고 말한다.모호한 선택을 피하는 방법 두 방식의 장점을 모두 가질 수는 없을까? 다시 말해서, 어떤상황에서는 이름에 의한 호출을 사용하고, 어떤 상황에서는 값에의한 호출을 사용할 수 없을까? 이 질문에 답한 수많은 선구자들가운데 폴 블레인 레비(Paul Blain Levy)가 내놓은 답인 "값밀기에 의한 호출"("Call-By-Push-Value", CBPV)은 함수형언어의 평가를 기계 수준(Machine level)에서 이해하는데 지대한발상의 전환을 제공했다. CBPV는 우선"계산"("Computation")과 "값"("Value")을구분한다.계산 MM, NN, LL, …\ldots = 함수 λx→M\lambda x \to M 또는 함수 호출 L VL\ V값 VV, UU, WW, …\ldots = 변수 xx<잠깐, 앞서서 함수형 언어에서 함수는 값이라고 하지 않았던가?이는 값 밀기에 의한 호출에서 함수와 함수 호출을 종전과전혀 다르게 이해하기 때문이다. 함수 λx→M\lambda x \to M는스택(Stack)에서 값을 빼내어(Pop) xx라는 이름을 붙인 후MM을 평가하는 것이고, 함수 호출 L VL\ V는 스택에 값 VV를밀어넣고(Push)[5] LL을 평가하는 것이다. 따라서 함수λx→M\lambda x \to M는 평가의 결과가 아닌 추가적인 평가가 가능한표현식이 된다. 이 구분을 간결하게 설명하는 것이 다음의 CBPV 표어이다.<값은 "~인 것"이다. 계산은 "~하는 것"이다.<그렇지만 함수형 언어이기 위해서는 함수를 값으로 취급할 수있어야 한다고 했지 않은가? 그렇다. 이를 위해 CBPV는<계산을 강제한다면(force\mathbf{force}) 계산 MM를 하는 지연된 계산인 값 thunk(M)\mathbf{thunk}(M)<을 추가로 제공한다. 이 둘(force(V)\mathbf{force}(V)와 thunk(M)\mathbf{thunk}(M))을 다음과 같이 문법에추가할 수 있다.계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V)값 = xx 또는 thunk(M)\mathbf{thunk}(M)<CBPV를 완성하기 위해 필요한 마지막 조각은 계산을 끝내는 법이다.현재까지 설명한 λx→M\lambda x \to M와 L VL\ V 그리고 force(V)\mathbf{force}(V)는 모두 다음 계산을 이어서 하는 표현식이고, 계산을 끝내는 방법을제공하지는 않는다. 예를 들어 λx→M\lambda x \to M의 평가는 스택에서값을 빼내고 계산 MM의 평가를 이어한다. 그렇다면 계산의 끝은무엇인가? 결과 값을 제공하는 것이다. 이를 위해 return(V)\mathbf{return}(V)를계산에 추가하고, 이 결과 값을 사용할 수 있도록M to x→NM\ \mathbf{to}\ x \to N (계산 MM을 평가한 결과 값을 xx라고 할 때계산 NN을 평가하는 계산) 또한 계산에 추가하면 다음의 완성된 CBPV를얻는다.계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V)또는 return(V)\mathbf{return}(V) 또는 M to x→NM\ \mathtt{\mathbf{to}}\ x \to N값 = xx 또는 thunk(M)\mathbf{thunk}(M)<이제 CBPV를 얻었으니 원래의 목표로 돌아가보자. 어떻게 CBV 호출과CBN 호출을 CBPV로 설명할 수 있을까?CBV 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를return(thunk(λx→M))\mathbf{return}{(\mathbf{thunk}(\lambda x \to M))}과L to x→N to y→force(x) yL\ \mathbf{to}\ x \to N\ \mathbf{to}\ y \to \mathbf{force}(x)\ y로표현할 수 있다. 즉, CBPV의 관점에서 CBV의 함수는 지연된 원래 계산λx→M\lambda x \to M을 값으로 되돌려주는 계산으로 이해할 수 있고, 함수호출 L NL\ N은 함수 부분 LL을 먼저 평가하고 NN을 평가한 뒤 NN의계산 결과 yy를 스택에 밀어넣고 지연된 계산인 함수부분 xx의 계산을 강제하는(force(x)\mathbf{force}(x)) 것으로 이해할 수있다.CBN 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를λx→M\lambda x \to M(단, 변수 xx의 모든 사용을 force(x)\mathbf{force}(x)로치환함)과 L thunk(N)L\ \mathbf{thunk}(N)로 표현할 수 있다.즉, CBPV의 관점에서 함수 호출은 L NL\ N은 지연된 NN을스택에 밀어넣은 뒤 LL의 계산을 이어가는 것으로 볼 수 있다. 이 지연된 NN은이후에 스택에서 빼내어져 어떤 이름 xx가 붙은 뒤, 이 변수가 사용될때에야 비로소 계산된다.<다소 설명이 복잡할 수 있으나, 단순하게 말해서 CBPV는 CBV에 따른상세한 평가 순서와 CBN 따른 상세한 평가 순서를 세부적으로 설명할 수있는 충분한 기능을 모두 갖추고 있으며, 이를 통해 CBV 함수 호출과 CBN함수 호출을 모두 설명할 수 있다는 이야기이다.기계 수준(Machine level)에서의 Call-By-Push-Value의 장점 앞에서는 CBPV가 CBV와 CBN를 모두 설명할 수 있음을 다뤘다.그러나 CBPV는 프로그래머(Programmer)가 직접 사용하기에는 과도하게자세한 세부사항들을 포함하고 있기에, 프로그래머가 직접 CBPV를 써서CBV와 CBN의 구분을 조율하기에는 적합하지 않다. 그렇다면 어느 수준에서CBV와 CBN을 혼합해 사용할 때 도움을 줄 수 있을까? 바로 람다 대수를기계 수준으로 컴파일(Compile)할 때이다. 이때는 CBPV가 가진 자세한세부사항의 표현력이 굉장히 유용해진다. 예를 들어 람다 대수를 기계 수준으로 변환할 때 흔히 필요한 것 중 하나인항수 분석(Arity analysis)에 대해 이야기해보자. 항수 분석은 함수가 하나의인자를 받은 뒤 실행되어야 하는지, 혹은 두 인자를 모두 받아 실행되어야 하는지등을 확인하여 이후에 그에 걸맞는 최적화된 기계어(Machine language)를 생성할수 있게 도와주는 분석 작업이다. 평범한 람다 대수에서는 항수 분석의 결과를직접적으로 표현하기 어렵다. 예를 들어 람다 대수의λx→(λy→y)\lambda x \to (\lambda y \to y)의 경우 이 함수가 xx와 yy를 모두받아 yy를 되돌려주는 함수인지 (항수가 2인 함수인지), 혹은 xx를 받아λy→y\lambda y \to y라는 함수를 되돌려주는 함수인지 (항수가 1인 함수인지)구분할 수 없다. 그러나 이를 CBPV로 변환한λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))나λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는각각이 무엇을 뜻하는지 분명히 이해할 수 있다.λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))는두 변수 xx와 yy를 스택에서 빼낸 뒤 yy의 값을 되돌려주는 함수(항수가 2인 함수)이다.λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는변수 xx를 스택에서 빼낸 뒤 지연된 계산 λy→return(y)\lambda y \to \mathtt{return}(y)를돌려주는 함수(항수가 1인 함수)이다.<이런 장점을 바탕으로 CBPV를 더 발전시킨"언박싱한 값에 의한 호출"("Call-By-Unboxed-Value")을GHC 컴파일러의 중간 언어(Intermediate language)로 구현하는것에 대한 논의가 현재 진행되고 있으며 앞으로 더 많은함수형 컴파일러들이 관련된 중간 언어를 채용하기 시작할 것으로보인다.<마치며 이 글에서는 함수형 언어의 핵인 람다 대수를 간단히 설명하고람다 대수를 평가하는 방법에 대해서 다루어보았다. 특히 그 중값 밀기에 의한 평가(Call-By-Push-Value, CBPV)가 무엇이며CBPV가 다른 대표적인 두 방법(CBV, CBN)을 어떻게 표현할 수있는지, 그리고 CBPV의 장점이 무엇인지에 대해서도 다루어보았다. 이 글에서 미처 다루지 못한 중요한 주제는 CBPV를기계에 가까운 언어로 번역해보는 것이다. 여기에서는 글이너무 복잡해지는 것을 피하기 위해 제했으나, CBPV의 장점에서살펴봤듯 이는 CBPV에 있어 핵심 주제 중 하나이기 때문에이후에 다른 글을 통해서라도 이 주제를 소개할 기회를 가지고자한다. 이 글이 CBPV에 대한 친절한 소개글이었기를 바라며이만 줄이도록 하겠다. 결과 값(Value)을 가지는 언어 표현을 말한다.예를 들어 1+11 + 1은 22라는 값을 가지는 표현식이지만(JavaScript의) let x = 3;나 (Python의)def f(): ...은 그 자체로는 값이 없기 때문에 표현식이아니다. ↩︎ 다만 실제 역사에서는 람다 대수의 이해와발견이 함수형 언어의 개발보다 먼저 이루어졌다.이런 역사적 관점에서는 (이미 많은 수학자들이이해하고 있던) 람다 대수에 여러 기능을 추가한것이 바로 함수형 언어라고 볼 수 있다. ↩︎ 프로그래밍 언어(Programming Language)는 실제로는치환을 사용하지 않고 환경(Environment)을 사용하는 경우가더 많지만 설명의 편의를 위해 다른 언어들 또한 환경 대신치환에 기반해 평가한다고 가정하겠다. ↩︎ 앞서 설명한 람다 대수에서는 이를 쉽게 얻을 수 있다.오메가(Ω\Omega)라고 부르는 표현식인(λx→x x) (λx→x x)(\lambda x \to x\ x)\ (\lambda x \to x\ x)의 평가는값에 의한 호출을 따르든 이름에 의한 호출을 따르든 종료되지않는다. ↩︎ 바로 이 함수 호출을 값 밀기에 기반해 해석하는 데에서 CBPV의 이름이 유래했다. ↩︎

Hackers' Pub

Фундаментальная математика — теория всего в IT и не только. Теория типов и формализация в Coq

У нас есть 3 "теории всего" - научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике). Именно фундамент математики представляет особый интерес, так как он является фундаментом для двух других фундаментов и имеет глубокий философский смысл. Последние 2 года я сильно им увлекся и проделал довольно большую работу по углубленному изучению теории типов (Calculus of Constructions), и готов поделиться результатами, а также рассказать о девяти направлениях, где можно применить это на практике. Очень многое получилось лучше, чем я планировал. Изначально перспективы были не очень понятными, и поэтому я не рассказывал друзьям и коллегам про мою работу в этом направлении и называл это "Секретный Проект". Но теперь, когда многое прояснилось и получилось, можно поделиться успехом. Собственно, в этой статье я расскажу вам не только про сам фундамент математики, а еще его связь с ежедневной работой программиста, а также с Computer Science/Data Science и AI/ML. Я вам нарисую большую и красивую картину, на которой все понятно и логически следует из маленького набора правил выведений типов (11 штук) и аксиом теории множеств (9 штук). У нас есть 3 фундамента математики - теория множеств (удобна для человека), теория типов (удобна для компьютера) и теория категорий (не знаю, зачем она вообще нужна). Они примерно одинаковой мощности и одну можно выразить внутри другой. Особый интерс представляет именно теория типов, тк ее довольно легко можно запрограммировать внутри компьютера и использовать как строгий фундамент для других теорий, который не дает совершить ошибку и проверяет каждое ваше действие.

https://habr.com/ru/articles/870592/

#Calculus_of_constructions #coq #type_theory #lambda_calculus #theorem_prover #фундамент_знаний #Фундамент_математики #zfc

Фундаментальная математика — теория всего в IT и не только. Теория типов и формализация в Coq

У нас есть 3 "теории всего" - научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике). Именно фундамент математики...

Хабр
A framework for defining logics | Journal of the ACM

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...

Journal of the ACM
Theorems for free! | Proceedings of the fourth international conference on Functional programming languages and computer architecture

ACM Conferences
Theorems for free! | Proceedings of the fourth international conference on Functional programming languages and computer architecture

ACM Conferences
A framework for defining logics | Journal of the ACM

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...

Journal of the ACM
A framework for defining logics | Journal of the ACM

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...

Journal of the ACM

I feel like @cosmician is turning to the dark side of Math which is lambda calculus.

#math #mathematics #lambda #calculus #lambda_calculus