{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ ":opt no-lint" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# $\\lambda$-calculus with arithmetic expressions\n", "\n", "람다계산법은 수리명제자동판별문제(Entscheidungsproblem)의 해결 불가능함을 보이기 위해\n", "Alonzo Church가 최소한의 문법으로 고안한 이론적 소품으로써 탄생했다.\n", "이후 프로그래밍 언어 이론의 연구에 활발히 활용되고 있으며\n", "특히 *함수형 프로그래밍 언어*(functional programming language) 설계의 기초가 되고 있다.\n", "\n", "이론적으로 순수한 람다계산법으로도 조건문, 자연수 계산 등 모든 것이 표현 가능하긴 하지만\n", "순수한 람다계산법만으로 실제 컴퓨터에서 계산을 돌린다면 비효율적 수 있다.\n", "컴퓨터 하드웨어에서 제공하는 정수 연산 등 여러 가지 다양한 기능을\n", "람다계산법을 기초로 하여 덧붙여 나간 언어들이 바로 함수형 프로그래밍 언어이다.\n", "또한 최근에는 함수형 프로그래밍 언어로 시작하지 않은 많은 프로그래밍 언어들이\n", "람다계산법의 문법이나 개념을 도입하고 있기도 하므로 실무적 프로그래밍 능력 향상을 위해서도\n", "람다계산법에 대한 기본적 이해가 있어야 한다.\n", "\n", "이 노트북에서는 지금까지 살펴본 덧셈식과 람다계산법을 같이 함께 합쳐 놓은 언어에 대한\n", "call-by-value 인터프리터를 작성한다." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "$x,y,z,\\ldots \\in \\textsf{Nm} = \\textsf{String}$\n", "\n", "$n \\in \\textsf{Int}$\n", "\n", "$\\begin{array}{lrl}\n", " e \\in \\textsf{Tm}\n", " &::=& x ~\\mid~ \\lambda x.e ~\\mid e_1~e_2 \\\\\n", " &\\mid& n ~\\mid~ e_1 ✚\\, e_2 \\\\\n", " &\\mid& \\textbf{if}~e~\\textbf{then}~e_1~\\textbf{else}~e_0\n", " \\end{array}$\n", "\n", "$\\textsf{Env} = \\textsf{Nm} \\xrightarrow{\\textrm{fin}} \\textsf{Value}$\n", "\n", "$\\sigma \\in \\textsf{Env} ::= \\{x_1\\mapsto v_1,\\ldots,x_n\\mapsto v_n\\}$\n", "\n", "$\\textsf{Value} \\subsetneq (\\textsf{Env} \\times \\textsf{Tm}) \\;\\cup\\; \\textsf{Int}$\n", "\n", "$v \\in \\textsf{Value} ::= \\langle \\sigma, \\lambda x.e \\rangle ~\\mid~ n$" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "$\\displaystyle\n", "\\frac{}{\\sigma,x \\Downarrow \\sigma(x)} \\qquad\n", "\\frac{}{\\sigma,\\lambda x.e \\Downarrow \\langle\\sigma,\\lambda x.e\\rangle}\n", "$\n", "\n", "$\\displaystyle\n", "\\frac{\n", " \\sigma,e_1 \\Downarrow \\langle\\sigma_1,\\lambda x.e\\rangle\n", " \\quad\n", " \\sigma,e_2 \\Downarrow v_2 \\quad \\{x\\mapsto v_2\\}\\sigma_1, e \\Downarrow v\n", " }{\\sigma,e_1~e_2 \\Downarrow v}\n", "$\n", "\n", "$\\displaystyle\n", " \\frac{~~}{\\sigma,n \\Downarrow n}\n", " \\qquad\n", " \\frac{\\sigma,e_1 \\Downarrow n_1 \\quad \\sigma,e_2 \\Downarrow n_2}{\n", " \\sigma,e_1 ✚\\, e_2 \\Downarrow n_1+n_2}$\n", " \n", "$\\displaystyle\n", " \\frac{\\sigma,e \\Downarrow 0 \\quad \\sigma,e_0 \\Downarrow n_0}{\n", " \\sigma,\\texttt{if}~ e ~\\texttt{then}~ e_1 ~\\texttt{else}~ e_0 \\Downarrow n_0}\n", " \\qquad \n", " \\frac{\\sigma,e \\Downarrow n \\quad \\sigma,e_1 \\Downarrow n_1}{\n", " \\sigma,\\texttt{if}~ e ~\\texttt{then}~ e_1 ~\\texttt{else}~ e_0 \\Downarrow n_1}~(n\\neq 0)$\n" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [], "source": [ "-- 변수 이름은 문자열 나타낸다\n", "type Nm = String\n", "\n", "-- 람다식 문법 구조\n", "data Tm = Var Nm -- x\n", " | Lam Nm Tm -- (λx.e)\n", " | App Tm Tm -- (e1 e2)\n", " | Val Int -- n\n", " | Add Tm Tm -- e1 + e2\n", " | If Tm Tm Tm -- if e then e1 else e0\n", " deriving (Show, Eq)" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [], "source": [ "-- 람다식을 보기좋게 문자열로 변환해주는 함수\n", "ppTm (Var x) = x\n", "ppTm (Lam x e) = \"\\\\\" ++ x ++ \" -> \" ++ ppTm e\n", "ppTm (App e1 e2) = pp1 e1 ++ \" \" ++ pp2 e2\n", "ppTm (Val n) = show n\n", "ppTm (Add e1 e2) = ppp e1 ++ \" + \" ++ ppp e2\n", "ppTm (If e e1 e0) = \"if \"++pp2 e++\" then \"++pp2 e1++\" else \"++pp2 e0 \n", "\n", "pp1 e@(Lam{}) = paren (ppTm e)\n", "pp1 e@(Add{}) = paren (ppTm e)\n", "pp1 e@(If{}) = paren (ppTm e)\n", "pp1 e = ppTm e\n", "\n", "pp2 e@(Var{}) = ppTm e\n", "pp2 e@(Val{}) = ppTm e\n", "pp2 e = paren (ppTm e)\n", "\n", "ppp e@(Var{}) = ppTm e\n", "ppp e@(Val{}) = ppTm e\n", "ppp e@(Add{}) = ppTm e\n", "ppp e@(App{}) = ppTm e\n", "ppp e = paren (ppTm e)\n", "\n", "paren s = \"(\" ++ s ++ \")\"\n", "brack s = \"[\" ++ s ++ \"]\"\n", "latex s = \"$\" ++ s ++ \"$\"\n", "\n", "-- 람다식을 보기좋게 TeX 코드로 변환해주는 함수\n", "texTm (Var x) = x\n", "texTm (Lam x e) = \"\\\\lambda \" ++ x ++ \".\" ++ texTm e\n", "texTm (App e1 e2) = tex1 e1 ++ \"~\" ++ tex2 e2\n", "texTm (Val n) = show n\n", "texTm (Add e1 e2) = texp e1 ++ \"+\" ++ texp e2\n", "texTm (If e e1 e0) = \"\\\\texttt{if}~\"++tex2 e++\"~\\\\texttt{then}~\"++tex2 e1++\"~\\\\texttt{else}~\"++tex2 e0\n", "\n", "tex1 e@(Lam{}) = paren (texTm e)\n", "tex1 e@(Add{}) = paren (texTm e)\n", "tex1 e@(If{}) = paren (texTm e)\n", "tex1 t = texTm t\n", "\n", "tex2 s@(Var{}) = texTm s\n", "tex2 s@(Val{}) = texTm s\n", "tex2 s = paren (texTm s)\n", "\n", "texp s@(Var{}) = texTm s\n", "texp s@(Val{}) = texTm s\n", "texp s@(Add{}) = texTm s\n", "texp s@(App{}) = texTm s\n", "texp s = paren (texTm s)" ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\\x -> x" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\\x -> \\y -> x" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\\x -> \\y -> y" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "if (3 + x + y) then (\\x -> \\y -> y) else ((\\x -> x) (\\x -> \\y -> x))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "idTm = Lam \"x\" (Var \"x\")\n", "ttTm = Lam \"x\" (Lam \"y\" (Var \"x\")) \n", "ffTm = Lam \"x\" (Lam \"y\" (Var \"y\")) \n", "\n", "putStr $ ppTm idTm\n", "putStr $ ppTm ttTm\n", "putStr $ ppTm ffTm\n", "putStr $ ppTm (If (Add (Val 3) (Add (Var \"x\") (Var \"y\"))) ffTm (App idTm ttTm))" ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\lambda x.x$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\lambda x.\\lambda y.x$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\lambda x.\\lambda y.y$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$x~y~z$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$x~(y~z)$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$(\\lambda x.\\lambda y.y)~(\\lambda x.x)~(\\lambda x.\\lambda y.x)$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\texttt{if}~(3+x+y)~\\texttt{then}~(\\lambda x.\\lambda y.y)~\\texttt{else}~((\\lambda x.x)~(\\lambda x.\\lambda y.x))$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "import IHaskell.Display\n", "\n", "html . latex $ texTm idTm\n", "html . latex $ texTm ttTm\n", "html . latex $ texTm ffTm\n", "html . latex $ texTm (App (App (Var \"x\") (Var \"y\")) (Var \"z\"))\n", "html . latex $ texTm (App (Var \"x\") (App (Var \"y\") (Var \"z\")))\n", "html . latex $ texTm (App (App ffTm idTm) ttTm)\n", "html . latex $ texTm (If (Add (Val 3) (Add (Var \"x\") (Var \"y\"))) ffTm (App idTm ttTm))" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [], "source": [ "-- call-by-value evaluator\n", "type Env = [ (Nm, Value) ]\n", "data Value = Clos Env Tm\n", " | Vint Int\n", " deriving Show\n", "\n", "eval :: Env -> Tm -> Value\n", "eval env (Var x) =\n", " case lookup x env of\n", " Nothing -> error (x ++ \" not defined\")\n", " Just v -> v\n", "eval env e@(Lam _ _) = Clos env e\n", "eval env (App e1 e2) =\n", " case v1 of\n", " Clos env1 (Lam x e) -> eval ((x,v2):env1) e\n", " _ -> error (show v1++\" not Lam\")\n", " where\n", " v1 = eval env e1\n", " v2 = eval env e2\n", "eval env (Val n) = Vint n\n", "eval env (Add e1 e2) =\n", " case (v1, v2) of\n", " (Vint n1, Vint n2) -> Vint (n1 + n2)\n", " (Vint _ , _ ) -> error (show v2++\" not int\")\n", " _ -> error (show v1++\" not int\")\n", " where\n", " v1 = eval env e1\n", " v2 = eval env e2\n", "eval env (If e e1 e0) =\n", " case eval env e of\n", " Vint n -> if n==0 then eval env e0\n", " else eval env e1\n", " _ -> error (show e++\" not int\")\n", "eval env e =\n", " error (show e ++ \" evaluation not defined yet\")" ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [], "source": [ "import Data.List (intersperse)\n", "\n", "texValue (Clos env e) = \"\\\\langle\"++texEnv env++\",\"++texTm e++\"\\\\rangle\"\n", "texValue (Vint n) = show n\n", "\n", "texEnv env = \"\\\\{\"\n", " ++ (concat . intersperse \",\")\n", " [x++\"\\\\mapsto \"++texValue v | (x,v) <-env]\n", " ++ \"\\\\}\"" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\langle\\{\\},\\lambda x.\\lambda y.\\texttt{if}~x~\\texttt{then}~(x+y)~\\texttt{else}~(y+y)\\rangle$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$2$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$3$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "e1 = Lam \"x\" $ Lam \"y\" $\n", " If (Var \"x\") (Add (Var \"x\") (Var \"y\"))\n", " (Add (Var \"y\") (Var \"y\"))\n", "\n", "e2 = Val 2\n", "e3 = Val 3\n", "\n", "html . latex . texValue $ eval [] e1\n", "html . latex . texValue $ eval [] e2\n", "html . latex . texValue $ eval [] e3" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda x.\\lambda y.\\texttt{if}~x~\\texttt{then}~(x+y)~\\texttt{else}~(y+y))~2$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{x\\mapsto 2\\},\\lambda y.\\texttt{if}~x~\\texttt{then}~(x+y)~\\texttt{else}~(y+y)\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex $ texTm (App e1 e2)\n", "html . latex . texValue $ eval [] (App e1 e2)" ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda x.\\lambda y.\\texttt{if}~x~\\texttt{then}~(x+y)~\\texttt{else}~(y+y))~2~3$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$5$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex $ texTm (App (App e1 e2) e3)\n", "html . latex . texValue $ eval [] (App (App e1 e2) e3)" ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda x.\\lambda y.\\texttt{if}~x~\\texttt{then}~(x+y)~\\texttt{else}~(y+y))~0~3$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$6$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex $ texTm (App (App e1 (Val 0)) e3)\n", "html . latex . texValue $ eval [] (App (App e1 (Val 0)) e3)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "---\n", "## Recursion using a fixpoint combinator\n", "\n", "$f(x)=x$를 만족하는 $x$를 함수 $f$의 fixpoint라고 말한다.\n", "\n", "fixpoint combinator란 람다계산법에서 임의의 함수 $f$에 대해 $f$의 fixpoint를 찾아주는 역할을 하는 고차함수라고 생각하면 된다.\n", "\n", "$Z$가 fixpoint combinator라는 말은 $Z(f)$가 $f$의 fixpoint 즉 $f(Z(f)) = Z(f)$라는 뜻이다.\n", "\n", "람다계산법에서는 함수 적용에 괄호를 쓰지 않으므로 $f(Z~f) = Z~f$ 이렇게 표기하는 경우가 더 많을 것이다.\n", "\n", "이것을 반대 방향으로 진행해보면 $Z~f = f(Z~f) = f(f(Z~f)) = f(f(f(Z~f))) = \\cdots$\n", "이렇게 함수 $f$를 몇번이고 반복 적용하는 계산을 표현할 수 있다." ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\lambda f.(\\lambda x.f~(\\lambda z.x~x~z))~(\\lambda x.f~(\\lambda z.x~x~z))$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "-- Z = λf.(λx.f(λz.xxz))(λx.f(λz.xxz))\n", "cZ = Lam \"f\" (App e e)\n", " where\n", " e = Lam \"x\" $ f `App` Lam \"z\" (App x x `App` z)\n", " f = Var \"f\"\n", " x = Var \"x\"\n", " z = Var \"z\"\n", "\n", "html . latex . texTm $ cZ" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\lambda f.\\lambda i.\\texttt{if}~i~\\texttt{then}~(i+f~(i+-1))~\\texttt{else}~i$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "-- λf.λi.if i then i + f(i + -1) else i\n", "e4 = Lam \"f\" . Lam \"i\" $ If i (i `Add` App f (i `Add` Val (-1))) i \n", " where\n", " f = Var \"f\"\n", " i = Var \"i\"\n", "\n", "html . latex . texTm $ e4" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Vint 5050" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "-- Z (λf.λi.if i then i + f(i + -1) else i) 100\n", "eval [] (App cZ e4 `App` Val 100) -- 100부터 0까지의 총합" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "100은 너무 길어지니까 2정도로만 람다식을 손으로 전개해 보자.\n", "\n", "```\n", "cZ e4 2\n", "= (λf.(λx.f(λz.xxz)) (λx.f(λz.xxz))) e4 2\n", "= (λx.e4(λz.xxz)) (λx.e4(λz.xxz)) 2 여기서 w = (λx.e4(λz.xxz))라고 하자\n", "= (λx.e4(λz.xxz)) w 2\n", "= e4 (λz.w w z) 2\n", "= (λf.λi.if i then i + f (i + -1) else i) (λz.w w z) 2\n", "= (λi.if i then i + (λz.w w z) (i + -1) else i) 2\n", "= if 2 then 2 + (λz.w w z) (2 + -1) else 2\n", "= 2 + (λz.w w z) 1\n", "= 2 + w w 1\n", "= 2 + (λx.e4(λz.xxz)) w 1\n", "= 2 + e4 (λz.w w z) 1\n", "= 2 + (λf.λi.if i then i + f (i + -1) else i) (λz.w w z) 1\n", "= 2 + (λi.if i then i + (λz.w w z) (i + -1) else i) 1\n", "= 2 + if 1 then 1 + (λz.w w z) (1 + -1) else 1\n", "= 2 + 1 + (λz.w w z) (1 + -1)\n", "= 2 + 1 + w w 0\n", "= 2 + 1 + (λx.e4(λz.xxz)) w 0\n", "= 2 + 1 + e4 (λz.w w z) 0\n", "= 2 + 1 + (λf.λi.if i then i + f (i + -1) else i) (λz.w w z) 0\n", "= ...\n", "= 2 + 1 + if 0 then 0 + f (0 + -1) else 0\n", "= 2 + 1 + 0\n", "```\n", "\n", "\n", "참고로 $Y=\\lambda f.(\\lambda x.f(xx))(\\lambda x.f(xx))$라는 $Z$보다 조금 더 간단한 fixpoint combinator가 있다.\n", "그런데 call-by-value 또는 applicative-order 계산 방식에서는 이 $Y$-combinator는 계산을 끝내지 못하고 무한히 진행되기만 한다.\n", "$Z$-combinator는 그래서 call-by-value 또는 applicative-order 에서도 재귀적 계산을 표현하는 데 활용할 수 있다.\n", "$Y$나 $Z$ 말고도 람다계산법에서 fixpoint-combinator들이 더 존재한다." ] }, { "cell_type": "code", "execution_count": 17, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda f.(\\lambda x.f~(\\lambda z.x~x~z))~(\\lambda x.f~(\\lambda z.x~x~z)))~(\\lambda f.\\lambda i.\\texttt{if}~i~\\texttt{then}~(i+f~(i+-1))~\\texttt{else}~i)$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "e11 = App cZ . Lam \"g \" . Lam \"n\" . App cZ . Lam \"f\" . Lam \"i\" $\n", " If (Add n i) (If \n", " (Val 0) \n", " where\n", " n = Var \"n\"\n", " f = Var \"f\"\n", " i = Var \"i\"\n", "\n", "html . latex . texTm $ e11" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Haskell", "language": "haskell", "name": "haskell" }, "language_info": { "codemirror_mode": "ihaskell", "file_extension": ".hs", "name": "haskell", "pygments_lexer": "Haskell", "version": "8.6.5" } }, "nbformat": 4, "nbformat_minor": 4 }