{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ ":opt no-lint" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# $\\lambda$-calculus evaluator" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## 표준화(normalization) vs. 값계산(evaluation)\n", " * 표준화 - 람다로 시작하는 함수정의식 안까지 들어가서 식을 줄임\n", " - normal-order reduction
\n", " $(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))\n", " \\\\ \\longrightarrow\n", " \\lambda z.(\\lambda x.(\\lambda v.v)~(\\lambda w.w)~x)~z\n", " \\\\ \\longrightarrow\n", " \\lambda z.(\\lambda v.v)~(\\lambda w.w)~z\n", " \\\\ \\longrightarrow\n", " \\lambda z.(\\lambda w.w)~z\n", " \\\\ \\longrightarrow\n", " \\lambda z.z\n", " \\\\ ~\n", " $\n", " - applicative-order reduction
\n", " $(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))\n", " \\\\ \\longrightarrow\n", " (\\lambda f.\\lambda z.f~z)~((\\lambda v.v)~(\\lambda w.w))\n", " \\\\ \\longrightarrow\n", " (\\lambda f.\\lambda z.f~z)~(\\lambda w.w)\n", " \\\\ \\longrightarrow\n", " \\lambda z.(\\lambda w.w)~z\n", " \\\\ \\longrightarrow\n", " \\lambda z.z\n", " \\\\ ~\n", " $\n", " \n", " * 값계산 - 함수를 더 이상 계산 진행 필요없는 값으로 보고 함수정의식 안까지는 들어가지 않고 식을 줄임\n", " - call-by-name evaluation
\n", " $(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))\n", " \\\\ \\longrightarrow\n", " \\lambda z.(\\lambda x.(\\lambda v.v)~(\\lambda w.w)~x)~z\n", " $\n", " \n", " - call-by-need evaluation (lazy evaluation)
\n", " call-by-name의 약점인 불필요한 계산 반복을 보완한 값계산 방법으로 나중에 소개한다.
\n", " \n", " - call-by-value evaluation (eager evaluation)
\n", " $(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))\n", " \\\\ \\longrightarrow\n", " (\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~(\\lambda w.w)\n", " \\\\ \\longrightarrow\n", " \\lambda z.(\\lambda x.(\\lambda w.w)~x)~z\n", " $" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "call-by-value 값계산의 약점은 굳이 할 필요 없는 계산을 하는 경우가 있다는 것.
\n", "$(\\lambda x.3)~(1+2+\\cdots+99999999+100000000)\n", "\\\\ \\longrightarrow \n", "\\cdots\\text{call-by-name 경우에 하지도 않을 필요없는 계산을 엄청나게 열심히 함}\\cdots\n", "\\\\ \\longrightarrow \n", "(\\lambda x.3)~5000000050000000\n", "\\\\ \\longrightarrow \n", "3\n", "$" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "call-by-name 값계산의 약점은 cbv보다 메모리를 더 많이 사용할 수도 있고\n", "또 그것보다 결정적인 문제는 반복하지 않아도 될 계산을 반복하는 경우가 있다는 것.
\n", "$(\\lambda x.x + x + x)~(3\\times 4)\n", "\\\\ \\longrightarrow\n", "(3\\times 4) + (3\\times 4) + (3\\times 4)\n", "\\\\ \\longrightarrow\n", "\\cdots\\text{cbv 경우에 1번만 했어도 될 곱하기를 3번 반복} \\cdots\n", "\\\\ \\longrightarrow\n", "12 + 12 + 12\n", "\\\\ \\longrightarrow\n", "\\cdots\n", "\\\\ \\longrightarrow\n", "36\n", "$" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "느긋한 값계산(lazy evaluation)이라고도 하는 call-by-need 값계산은\n", "call-by-name 값계산과 기본적으로 같은 방식으로 진행하되\n", "함수 적용시 매개변수를 인자식으로 바꿔넣는 것이 아니라 일단 포인터처럼\n", "처리하여 여러 번 사용되는 매개변수의 경우에 계산을 공유할 수 있도록 한다.\n", "
\n", "$\\{\\}~~ (\\lambda x.x + x + x)~(3\\times 4)\n", "\\\\ \\longrightarrow \n", "\\{x\\mapsto 3\\times 4\\}~~ x+x+x\n", "\\\\ \\longrightarrow \n", "\\{x\\mapsto 12\\}~~ 12+x+x\n", "\\\\ \\longrightarrow \n", "\\{x\\mapsto 12\\}~~ 12+12+x\n", "\\\\ \\longrightarrow \n", "\\{x\\mapsto 12\\}~~ 24+x\n", "\\\\ \\longrightarrow \n", "\\{x\\mapsto 12\\}~~ 24+12\n", "\\\\ \\longrightarrow \n", "\\{x\\mapsto 12\\}~~ 36\n", "$" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "지난번 노트북에서 사용하던 람다계산식 정의를 그대로 가져오자" ] }, { "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", " 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", " where\n", " pp1 e@(Lam{}) = paren (ppTm e)\n", " pp1 e = ppTm e\n", " pp2 e@(Var{}) = ppTm e\n", " pp2 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", " where\n", " tex1 e@(Lam{}) = paren (texTm e)\n", " tex1 t = texTm t\n", " tex2 s@(Var{}) = texTm s\n", " tex2 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" } ], "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" ] }, { "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": [ "$(\\lambda x.\\lambda y.y)~((\\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 (App ffTm (App idTm ttTm))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "$x,y,z,\\ldots \\in \\textit{Nm}$\n", "\n", "$e \\in \\textit{Tm} ::= x ~\\mid~ (\\lambda x.e) ~\\mid (e_1~e_2)$\n", "\n", "$\\textit{Env} = \\textit{Nm} \\xrightarrow{\\textrm{fin}} \\textit{Value}$\n", "\n", "$\\sigma \\in \\textit{Env} ::= \\{x_1\\mapsto v_1,\\ldots,x_n\\mapsto v_n\\}$\n", "\n", "$\\textit{Value} \\subsetneq \\textit{Env} \\times \\textit{Tm}$\n", "\n", "$v \\in \\textit{Value} ::= \\langle \\sigma, \\lambda x.e \\rangle$\n", "\n", "\n", "함수의 값을 나타내는 $\\langle \\sigma, \\lambda x.e \\rangle$에서\n", "실행환경 $\\sigma$는 함수정의식 $\\lambda x.e$의 자유변수들이\n", "어떤 의미인지 찾아볼 수 있도록 자유변수들의 의미가 열려 있지\n", "않게 닫아주는 (정확히 결정되도록 지정해주는) 역할을 한다.\n", "그래서 $\\langle \\sigma, \\lambda x.e \\rangle$를 closure라고 부른다.\n", "\n", "큰걸음 동작방식 의미론(big-step operational semantics)을 정의하는 추론규칙\n", "\n", "$\\displaystyle\n", "\\frac{\\displaystyle\n", " }{\\sigma,x \\Downarrow \\sigma(x)}\n", "\\qquad\n", "\\frac{\\displaystyle\n", " }{\\sigma,\\lambda x.e \\Downarrow \\langle\\sigma,\\lambda x.e\\rangle}\n", "\\\\~\\\\\\displaystyle\n", "\\frac{\\displaystyle\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", "$" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [], "source": [ "-- call-by-value evaluator\n", "type Env = [ (Nm, Value) ]\n", "data Value = Clos Env Tm 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" ] }, { "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", "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": [ "$(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "e1f = (Lam \"f\" $ Lam \"z\" $ App (Lam \"x\" $ Var \"f\" `App` Var \"x\") (Var \"z\"))\n", "e1a = (App (Lam \"v\" $ Var \"v\") (Lam \"w\" $ Var \"w\"))\n", "e1 = App e1f e1a\n", "\n", "html . latex . texTm $ e1" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\lambda f.\\lambda z.(\\lambda x.f~x)~z$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{\\},\\lambda f.\\lambda z.(\\lambda x.f~x)~z\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex . texTm $ e1f\n", "html . latex . texValue $ eval [] e1f" ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda v.v)~(\\lambda w.w)$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{\\},\\lambda w.w\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex . texTm $ e1a\n", "html . latex . texValue $ eval [] e1a" ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{f\\mapsto \\langle\\{\\},\\lambda w.w\\rangle\\},\\lambda z.(\\lambda x.f~x)~z\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex . texTm $ e1\n", "html . latex . texValue $ eval [] e1" ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))~(\\lambda x.x)$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{\\},\\lambda x.x\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "html . latex . texTm $ App e1 idTm\n", "html . latex . texValue $ eval [] (App e1 idTm)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "⟨{f↦⟨{},λw.w⟩},λz.(λx.f x) z⟩ 함수값에 ⟨{},λx.x⟩값을 인자로 호출\n", "\n", "{z↦⟨{},λx.x⟩, f↦⟨{},λw.w⟩}, (λx.f x) z ⇓ ??" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\{z\\mapsto \\langle\\{\\},\\lambda x.x\\rangle,f\\mapsto \\langle\\{\\},\\lambda w.w\\rangle\\}$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\lambda x.f~x$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "Clos [(\"z\",Clos [] (Lam \"x\" (Var \"x\"))),(\"f\",Clos [] (Lam \"w\" (Var \"w\")))] (Lam \"x\" (App (Var \"f\") (Var \"x\")))" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{z\\mapsto \\langle\\{\\},\\lambda x.x\\rangle,f\\mapsto \\langle\\{\\},\\lambda w.w\\rangle\\},\\lambda x.f~x\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "env2 = [ (\"z\", Clos [] (Lam \"x\" $ Var \"x\"))\n", " , (\"f\", Clos [] (Lam \"w\" $ Var \"w\"))\n", " ]\n", "\n", "html . latex . texEnv $ env2\n", "html . latex . texTm $ (Lam \"x\" $ Var \"f\" `App` Var \"x\")\n", "\n", "eval env2 (Lam \"x\" $ Var \"f\" `App` Var \"x\")\n", "\n", "html . latex . texValue $ eval env2 (Lam \"x\" $ Var \"f\" `App` Var \"x\")" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Clos [] (Lam \"x\" (Var \"x\"))" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "$\\langle\\{\\},\\lambda x.x\\rangle$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "eval env2 (Var \"z\")\n", "\n", "html . latex . texValue $ eval env2 (Var \"z\")" ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$\\{x\\mapsto \\langle\\{\\},\\lambda x.x\\rangle,z\\mapsto \\langle\\{\\},\\lambda x.x\\rangle,f\\mapsto \\langle\\{\\},\\lambda w.w\\rangle\\}$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "Clos [] (Lam \"x\" (Var \"x\"))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "env3 = (\"x\", Clos [] (Lam \"x\" (Var \"x\"))) : env2\n", "\n", "html . latex . texEnv $ env3\n", "\n", "eval env3 (App (Var \"f\") (Var \"x\"))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "----\n", "#### 연습문제 06-01\n", "\n", "실행 의미를 나타내는 규칙을 한번 더 복사해 왔다.\n", "\n", "$\\displaystyle\n", "\\frac{\\displaystyle\n", " }{\\sigma,x \\Downarrow \\sigma(x)}\n", "\\qquad\n", "\\frac{\\displaystyle\n", " }{\\sigma,\\lambda x.e \\Downarrow \\langle\\sigma,\\lambda x.e\\rangle}\n", "\\\\~\\\\\\displaystyle\n", "\\frac{\\displaystyle\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", "마지막에 살펴본 예제에 대한 동작방식 의미론 규칙 적용을 하나의 이어진 나무 형태로 나타내 보았다.\n", "\n", "$\\displaystyle\n", "\\frac{\n", " \\frac{\\normalsize\n", " \\vdots_{\\phantom{g_g}}\\qquad\n", " \\vdots_{\\phantom{g_g}}\\qquad\n", " \\vdots_{\\phantom{g_g}}\n", " }{\\footnotesize\n", " \\begin{array}{rr}\n", " \\{\\},(\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w)) \n", " \\Downarrow \\\\\n", " \\langle\\{f\\mapsto\\langle\\{\\},\\lambda w.w\\rangle\\},\\lambda z.(\\lambda x.f~x)~z\\rangle\n", " \\end{array} \n", " }\n", " ~\n", " \\frac{}{\\footnotesize\n", " \\begin{array}{rr}\n", " \\{\\},\\lambda x.x \\Downarrow \\\\\n", " \\langle\\{\\},\\lambda x.x\\rangle\n", " \\end{array}\n", " }\n", " ~\n", " \\frac{\\scriptsize\n", " \\frac{}{\\begin{array}{ll}\\{\\cdots\\}, \\lambda x.f~x \\Downarrow \\\\\n", " \\langle\\{\\cdots\\},\\lambda x.f~x\\rangle \\end{array}}\n", " \\frac{}{\\begin{array}{ll}\\{\\cdots\\}, z \\Downarrow \\\\\n", " \\langle\\{\\},\\lambda x.x\\rangle \\end{array}}\n", " ~\n", " \\frac{\\small\n", " \\vdots_{\\phantom{g_g}}\\qquad\n", " \\vdots_{\\phantom{g_g}}\\qquad\n", " \\vdots_{\\phantom{g_g}}\n", " }{\\begin{array}{rr}\n", " \\{x\\mapsto\\langle\\{\\},\\lambda x.x\\rangle,\\cdots\\}, f~x \\Downarrow \\\\\n", " \\color{blue}{\\langle\\{\\},\\lambda x.x\\rangle} \\end{array}}\n", " }{\\footnotesize\n", " \\begin{array}{rr}\n", " \\{ z\\mapsto\\langle\\{\\},\\lambda x.x\\rangle,\n", " f\\mapsto\\langle\\{\\},\\lambda w.w\\rangle \\}, (\\lambda x.f~x)~z \\Downarrow \\\\\n", " \\color{blue}{\\langle\\{\\},\\lambda x.x\\rangle}\n", " \\end{array}\n", " }\n", "}{\n", " \\{\\},\n", " (\\lambda f.\\lambda z.(\\lambda x.f~x)~z)~((\\lambda v.v)~(\\lambda w.w))\n", " ~(\\lambda x.x) \n", " \\Downarrow \\color{blue}{\\langle\\{\\},\\lambda x.x\\rangle}\n", "}$\n", "\n", "오른쪽 가지와 왼쪽 가지에 생략된 부분($\\footnotesize~\\vdots\\quad\\vdots\\quad\\vdots~$)들을 종이 연습장에 직접 한번 작성해 보라." ] }, { "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 }