{
"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
}