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