:opt no-lint
타입없는 람다계산법의 문법과 줄일 수 있는 식(reducible expression)의 개념 등에 대해 알아본다.
"줄일 수 있는 식"이라는 말이 너무 길기 때문에 '주는식'(redex)과 같은 줄임말을 보통 더 많이 사용한다.
$ x \in \textit{Nm} $
$ e \in \textit{Tm} \\ e ::=~ x ~\mid~ (\lambda x.e) ~\mid~ (e_1~e_2) $
보통 수학에서 $f(x) = x^2$과 같이 정의하는 함수 $f$를 람다계산법에서는 아래와 같은 방식으로 표현한다.
$(\lambda x.x^2)$
그리고 보통 수학에서 정의된 함수를 호출하는 $f(3)$과 같은 표현은 람다계산법에서는 괄호 없이 함수와 인자를 나열하여 아래와 같은 방식으로 표현한다.
$((\lambda x.x^2)~3)$
수학에서도 그렇듯 람다계산법에서도 어떤 함수가 다른 함수를 받아 또 다른 함수를 만들어낼 수 있다. 가장 대표적인 예로 '미분'이라는 개념을 함수를 받아 함수를 돌려주는 함수로 이해할 수도 있다.
$((미분~(\lambda x.x^2))~3) \longrightarrow\cdots\longrightarrow ((\lambda x.\,2\times x)~3) \longrightarrow 2\times 3 \longrightarrow 6$
물론 순수한 람다계산법에는 미분이나, 제곱, 곱하기, 등의 개념을 기본적으로 제공하지는 않으며 심지어 자연수도 기본 구성요소로 제공되지 않는다. 위에 예제는 개념적인 이해를 돕기 위한 설명이다. 참고로 Alonzo Church의 람다계산법은 Alan Turing의 튜링머신과 마찬가지로 괴델이 "수학명제 자동판별 문제"가 해결 불가능함을 증명한 불완전성 정리를 그들 나름의 방식으로 좀더 직접적으로 간략하게 증명하기 위한 이론적 도구 혹은 소품으로 만들어진 것이다. 가정하는 것이 아니라 하지만 이후 이런 소품들의 이론적 계산능력이 동일하다는 것이 밝혀지면서 오늘날 우리가 이해하는 컴퓨터로 할 수 있는 모든 계산의 이론적 범위를 발견한 것으로 받아들여지고 있는데 이를 처치-튜링 논제(Church-Turing thesis)라고 한다. 이와 관련한 역사적 배경 및 좀더 자세한 내용이 궁금한 사람들은 다음 온라인에 공개된 컴퓨터과학이 여는 세계 강의 시리즈의 1.4, 1.5, 1.6 내용 영상 등이 참고가 될 것이다.
-- 변수 이름은 문자열 나타낸다
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))
람다식의 부분식은 그 식의 일부로 나타나는 람다식이다. 전체 식 자체도 자기 자신의 부분식이라고 하자.
하스켈 데이타 타입 Tm으로 표현된 어떤 람다식의 부분식을 모두 나열하는 리스트를 구하는 함수를 다음과 같이 작성할 수 있다.
[2,3,4] ++ [7,8]
[2,3,4,7,8]
subTm :: Tm -> [Tm]
subTm (Var x) = [(Var x)] -- (Var x) : []
subTm (Lam x e1) = (Lam x e1) : subTm e1
subTm (App e1 e2) = (App e1 e2) : subTm e1 ++ subTm e2
e = App (Lam "x" (Var "x")) (Lam "y" (Var "y"))
html . latex . texTm $ e
subTm e
map (html . latex . texTm) (subTm e)
[App (Lam "x" (Var "x")) (Lam "y" (Var "y")),Lam "x" (Var "x"),Var "x",Lam "y" (Var "y"),Var "y"]
패턴매칭에서 부분별로 이름을 붙임과 동시에 구조 전체에도 이름을 붙여주려면 @을 활용한다.
예컨대 위의 subTm과 같은 함수를 다음과 @패턴을 활용하면 더 간결하게 정의되며,
컴파일러가 구조 전체를 함수 결과에서 그대로 참조할 수 있는 추가 정보가 돌 수 있으므로
컴파일된 코드의 성능이 개선될 가능성도 있다.
subTm' :: Tm -> [Tm]
subTm' e@(Var _) = [e]
subTm' e@(Lam x e1) = e : subTm e1
subTm' e@(App e1 e2) = e : subTm e1 ++ subTm e2
e = App (Lam "x" (Var "x")) (Lam "y" (Var "y"))
subTm' e
map (html . latex . texTm) (subTm' e)
[App (Lam "x" (Var "x")) (Lam "y" (Var "y")),Lam "x" (Var "x"),Var "x",Lam "y" (Var "y"),Var "y"]
람다계산법의 실행의미는 그 문법만큼이나 매우 단순하다. 함수정의식 $(\lambda x.e)$를 인자 $e_2$에 적용한 함수적용식 $((\lambda x.e)~e_2)$는 곧바로 줄일 수 있는 주는식(redex)이며 그것을 한 걸음 줄인 결과는 $e$에 나타나는 $x$를 $e_2$로 치환한 식, 즉 $x$의 자리에 $x$대신 $e_2$로 끼워넣은 식이 된다. 달리 말하지면 주는식이란 즉시 함수 호출을 할 수 있는 형태의 함수적용식을 말하는 것이다. 왜냐하면 즉시 함수 호출이 가능하려면 왼쪽에 오는 함수 부분이 람다로 시작하는 함수정의식이어야 하니까. 이러한 계산 규칙을 $\beta$-줄이기($\beta$-reduction)이라고 하며 아래와 같이 나타낸다. 참고로 줄이는 방법이 한 가지가 아니라 여러 가지 규칙이 포함된 람다계산법의 변이들도 가능한데 그런 경우 특정 규칙에 따라 주는식임을 표현하기 위해 $\beta$-주는식($\beta$-redex)이라고 줄이는 규칙의 이름을 앞에 붙여서 말하기도 한다.
$((\lambda x. e)~e_2) \longrightarrow \{x\mapsto e_2\}e$
여기에서 $\{x\mapsto e_2\}e$는 바로 $e$에서 $x$를 $e_2$로 치환한 식을 의미하는 표기법이다. 예컨대 $\big(\big(\lambda x.(\lambda y.(y~x)~x)\big)~z\big)$를 줄이면 $\{x\mapsto z\}(\lambda y.(y~x)~x)$ 그러니까 $(\lambda y.(y~z)~z)$가 된다.
참고로 위의 $\beta$-줄이기 규칙을 핵심으로 하되, 어떤 식이 그 자체로는 $\beta$-줄이기 규칙의 적용 대상이 아니더라도 규칙이 적용되는 부분을 찾아 그 부분의 식에 $\beta$-줄이기를 적용하는 규칙들을 추가로 정의할 수 있다. 예컨대, $\big(\big((\lambda x.x)~(\lambda y.y)\big)~(\lambda z.z)\big)$는 그 자체로는 식 전체에 $\beta$-줄이기 규칙을 적용할 수 없지만 그 부분식인 $\big((\lambda x.x)~(\lambda y.y)\big)$에는 $\beta$-줄이기 규칙을 적용할 수 있다. 사실 부분식에 $\beta$-줄이기를 어떻게 적용할지는 여러 가지 방법 혹은 전략이 가능한데 지금은 일단 적당히 아무 곳에나 적용한다고 하고 넘어가기로 하고 이후에 다시 이에 대해 생각해 보겠다.
하스켈 데이타 타입 Tm으로 표현된 어떤 람다식이
그 자체로 $\beta$-줄이기 규칙을 바로 적용할 수 있는 주는식(redex)인지
검사하는 함수를 다음과 같이 작성할 수 있다.
isRedEx :: Tm -> Bool
isRedEx (App (Lam{}) _) = True
isRedEx _ = False
e1 = idTm
e2 = App idTm idTm
e3 = (Lam "x" e2)
html . latex $ texTm e1
isRedEx e1
html . latex $ texTm e2
isRedEx e2
html . latex $ texTm e3
isRedEx e3
False
True
False
주어진 식 자체로는 주는식(redex)이 아니더라도 어떤 부분의 부분식에 주는식을 포함하고 있을 수도 있다.
그 자체로 주는 식인 경우 뿐만 아니라 부분식으로 주는식을 포함하는 식인지까지 검사하는 hasRedEx 함수를
다음과 같이 작성할 수 있다.
hasRedEx :: Tm -> Bool
hasRedEx (Var _) = False
hasRedEx (Lam _ e1) = hasRedEx e1
hasRedEx e@(App e1 e2) = isRedEx e || hasRedEx e1 || hasRedEx e2
e1 = idTm
e2 = App idTm idTm
e3 = (Lam "x" e2)
html . latex $ texTm e1
hasRedEx e1
html . latex $ texTm e2
hasRedEx e2
html . latex $ texTm e3
hasRedEx e3
False
True
True
참고로 위와 같은 일을 하는 다른 방법으로도 정의할 수 있다.
앞서 정의한 subTm 함수로 부분식을 모두 나열하여
그 중 하나라도 주는 식이 있는지 검사하는 isRedEx 함수와 함께
표준라이브러리 고차함수 any를 활용하면 알아볼 수 있으므로
똑같은 일을 하는 함수를 다음과 같이 정의할 수도 있다.
even 3
even 4
False
True
any even [1,3,5,7,9]
any even [1,3,4,7,9]
False
True
hasRedEx' = any isRedEx . subTm
e1 = idTm
e2 = App idTm idTm
e3 = (Lam "x" e2)
html . latex $ texTm e1
hasRedEx' e1
html . latex $ texTm e2
hasRedEx' e2
html . latex $ texTm e3
hasRedEx' e3
False
True
True
-- texTm을 적절히 변경하여 함수적용식 (e1 e2)에서
-- 함수 부분인 e1에 빨강 인자 부분인 e2에 파랑 사각형 테두리 추가
texTmColor (Var x) = x
texTmColor (Lam x e) = "\\lambda " ++ x ++ "." ++ texTmColor e
texTmColor (App e1 e2) = box1(tex1 e1) ++ "~" ++ box2(tex2 e2)
where
tex1 e@(Lam{}) = paren (texTmColor e)
tex1 t = texTmColor t
tex2 s@(Var{}) = texTmColor s
tex2 s = paren (texTmColor s)
box1 = red . boxed . black
box2 = blue . boxed . black
color c s = "\\color{"++c++"}{"++s++"}"
boxed s = "\\boxed{"++s++"}"
black = color "black"
red = color "red"
blue = color "blue"
e1 = Lam "f" (App idTm (App idTm (Var "f" `App` Var "f"))) `App` App idTm idTm
html . latex $ texTm e1
putStr $ texTmColor e1
html . latex $ texTmColor e1
\color{red}{\boxed{\color{black}{(\lambda f.\color{red}{\boxed{\color{black}{(\lambda x.x)}}}~\color{blue}{\boxed{\color{black}{(\color{red}{\boxed{\color{black}{(\lambda x.x)}}}~\color{blue}{\boxed{\color{black}{(\color{red}{\boxed{\color{black}{f}}}~\color{blue}{\boxed{\color{black}{f}}})}}})}}})}}}~\color{blue}{\boxed{\color{black}{(\color{red}{\boxed{\color{black}{(\lambda x.x)}}}~\color{blue}{\boxed{\color{black}{(\lambda x.x)}}})}}}
-- texTmRedEx :: Tm -> String
-- texTm을 적절히 변경하여 함수적용식 (e1 e2)에서
-- 함수 부분인 e1에 빨강 인자 부분인 e2에 파랑 사각형 테두리 추가
texTmRedEx (Var x) = x
texTmRedEx (Lam x e) = "\\lambda " ++ x ++ "." ++ texTmRedEx e
texTmRedEx e@(App e1 e2) =
if isRedEx e then box1(tex1 e1) ++ "~" ++ box2(tex2 e2)
else tex1 e1 ++ "~" ++ tex2 e2
where
tex1 e@(Lam{}) = paren (texTmRedEx e)
tex1 t = texTmRedEx t
tex2 s@(Var{}) = texTmRedEx s
tex2 s = paren (texTmRedEx s)
box1 = red . boxed . black
box2 = blue . boxed . black
e1 = Lam "f" (App idTm (App idTm (Var "f" `App` Var "f"))) `App` App idTm idTm
putStr $ texTmRedEx e1
html. latex $ texTmRedEx e1
\color{red}{\boxed{\color{black}{(\lambda f.\color{red}{\boxed{\color{black}{(\lambda x.x)}}}~\color{blue}{\boxed{\color{black}{(\color{red}{\boxed{\color{black}{(\lambda x.x)}}}~\color{blue}{\boxed{\color{black}{(f~f)}}})}}})}}}~\color{blue}{\boxed{\color{black}{(\color{red}{\boxed{\color{black}{(\lambda x.x)}}}~\color{blue}{\boxed{\color{black}{(\lambda x.x)}}})}}}
표준형은 규칙에 따라 더 이상 줄일 수 있는 부분식을 포함하지 않는 형태의 람다식을 말한다. 구체적으로 $\beta$-줄이기로 더 이상 줄일 수 있는 부분식이 전혀 포함하지 않는 람다식을 $\beta$-표준형이라 일컫는다.
주어진 람다식 $e$에 $\beta$-줄이기를 반복적으로 적용해 얻을 수 있는 $\beta$-표준형을 $e$의 $\beta$-표준형이라 말하는데, 타입없는 람다계산법에서는 주어진 람다식의 $\beta$-표준형이 존재한다면 유일하다는 처치-로서 정리(Church-Rosser theorem)가 성립힌다.
람다계산법의 처치-로서 정리를 직접 설명하기보다는 우선 직관적으로 처치-로서 정리가 어떤 성질을 의미하는지 덧셈식을 통해 간단히 개념만 알아보자.
예를 들어 (1 + 2) + (4 + 5) 라는 덧셈식이 있다면 어떤 덧셈을 먼저 하든 관계없이 항상 같은 결과값을 얻는다. 즉 덧셈식에서는 덧셈을 줄여나가는 것에 대한 처치-로서 정리의 성질이 성립한다고 말할 수 있다.
$(1 + 2) + (4 + 5) ~\longrightarrow~ 3 + (4 + 5) ~\longrightarrow~ 3 + 9 ~\longrightarrow~ 12$
$(1 + 2) + (4 + 5) ~\longrightarrow~ (1 + 2) + 9 ~\longrightarrow~ 3 + 9 ~\longrightarrow~ 12$
하지만 타입없는 람다계산법의 경우 계산이 일반적으로 항상 끝난다는 보장이 없다. 즉 어떤 람다식은 표준형이 아예 존재하지 않을 수도 있으며 표준형이 존재하더라도 어떤 줄일식을 먼저 계산하는가에 따라 계산이 끝날 수도 있고 끝나지 않을 수도 있다. 그래서 타입없는 람다계산법에서의 처치-로서 정리는 표준형이 존재하는 식의 경우 표준형에 도달할 수 있는 모든 계산 경로 끝에 있는 표준형이 모두 "같다"는 의미이다.
참고로 표준형이 없는 끝나지 않는 계산을 하는 대표적인 예가 바로 다음과 같은 람다식이다.
$ \big((\lambda x.x~x)~(\lambda x.x~x)\big) \longrightarrow \big((\lambda x.x~x)~(\lambda x.x~x)\big) \longrightarrow ~~\cdots$
잠깐, 근데 "같다"는 게 무엇인지 우리가 아직 정확히 정의하지 않았다.
일단 확실한 것은 글자 하나도 틀리지 않고 똑같으면 분명히 같은 것이다. 하지만 이것은 너무나 협소한 같음의 정의다. 왜냐하면 $(\lambda x.x)$와 $(\lambda y.y)$의 경우 비록 글자 하나하나를 비교하면 다른 점이 있기는 하지만 분명히 똑같은 식이라고 볼 수 있기 때문이다. $(\lambda x.x)$에서 함수 인자의 이름을 $x$대신 $y$로 바꾼 함수가 $(\lambda y.y)$이다. 이렇게 함수 인자의 이름을 일괄적으로 바꿔는 것을 $\alpha$-변환이라고 하며, 함수 인자 이름만 바꿔나가면 똑같아지는 관계에 있는 람다식들을 $\alpha$-동치 관계에 있다고 한다.
$((\lambda x.x)~(\lambda y.y))$와 $((\lambda y.(\lambda x.x))~z)$는 $\alpha$-동치가 아니다. 하지만 이를 $\beta$-줄이기로 한단계만 계산하면 계산 결과로 나오는 식들이 $\alpha$-동치임을 알 수 있다.
$((\lambda x.x)~(\lambda y.y)) \longrightarrow (\lambda y.y)$
$((\lambda y.(\lambda x.x))~z) \longrightarrow (\lambda x.x)$
이와 같이 $\beta$-줄이기를 (일반적으로는 한 걸음만 아니라 여러 걸음으로) 적용해서 같아지는 관계를 $\beta$-동치라고 한다. 덧셈식으로 비유하자면 ((3+4)+5)와 (2+(5+6))처럼 구조나 생김새가 설령 다르더라도 계산 결과가 같은 관계에 해당한다. 표준형이 있는 람다식끼리 비교하는 경우라면 처치-로서 정리의 성질에 의거해 서로의 표준형을 구해 같은지 알아봄으로써 $\beta$-동치 관계인지 검사가 가능하다.