[functional] fixed-pointer operator 가 무엇인지 알아야 아래

Lua를 전혀 몰라서 코드를 읽기가 몹시 우울하지만, 나머지 궁금해하시는 부분들에 대해서 최대한 간단하게 설명해보겠습니다. 코드의 의미와 연계시켜 이해하는 부분은 Lua를 잘 아시는 분께서 설명해주셔야할 것 같습니다.

코드에 나오는 Y function이란 combinatory logic의 Y combinator를 가리키는 것이로군요. Combinatory logic은 항상 λ-calculus를 따라다니는 이야기이므로 먼저 λ-calculus부터 설명하겠습니다. (λ-calculus는 그 자체만으로도 두꺼운 책 한 권을 쓸 수 있을만큼 깊고 관련 내용이 방대하지만, 지금은 다 필요 없습니다. 정확히 ‘기본’만, 그 중에서도 선택적으로 일부만 짚고 넘어가면 지금은 일단 충분하며, 아주 간단합니다!) 일단은 타입이 없는 untyped λ-calculus입니다:

• λ-term
  • (변수) 모든 변수 v는 λ-term입니다.
  • (함수 합성) 모든 변수 v와 모든 λ-term M에 대해서, λv.M 은 λ-term입니다. (정확하고 좋은 예시는 아니지만 C 프로그래머에게 밑그림이 되어줄만한 설명을 덧붙이자면, λv.M 이란 일단 대략 type_of(M) f(v) { return M; }
    정도로 받아들이시면 되겠습니다.)
    
  • (함수 적용) 모든 λ-term M과 N에 대해서, (M N)은 λ-term입니다. (이는 결국 전통적인 표기법으로는 M(N)에 해당하며 (그래서 ‘함수 적용’입니다), 이런 표기법을 juxtapositioning이라고 합니다. λ-calculus 뿐만 아니라 Haskell, ML 등 이를 기반으로하는 함수형 프로그래밍 언어들도 juxtapositioning을 쓰고있습니다.)
• 치환 규칙 (단, 자유변수와 종속변수에 대한 정확한 제한은 제외한 rough한 설명입니다)
  • (α-변환) λx.M은 λy.M[y/x] 와 같습니다. (단, M[y/x]란 M속에 자유변수로서 등장하는 모든 x들을 y로 싹 바꾼 결과입니다.) 역시 C 프로그래머용 설명을 덧붙이자면, 다음 두 개의 C 함수가 같은 계산을 의미하고 있음을 상기하시면 되겠습니다:

    int succ1(x) { return x + 1; }
    int succ2(y) { return y + 1; }

    
    
  • (β-치환) λv.M N은 M[N/v]이랑 같습니다. 역시 다음 C 함수 "호출"과 그 값을 계산하는 과정을 생각하시면 됩니다:

    succ1(5);
    5 + 1;

    
    즉, λv.M N을 M[N/v]으로 β-치환한다는 것은 결국 인수 N에 함수 λv.M을 적용한 (조금 더 C스러운 다른 말로는, 함수 λv.M을 인수 N을 주어 호출한) 결과를 ‘계산’하는 것입니다.
    
  • (η-치환) 어떤 두 람다 텀 M1과 M2가 있을 때, 만일 모든 람다 텀 N에 대해서 M1 N = M2 N이면 M1 = M2입니다. 이 부분은 사실은 자동 타입 추론 (inference, 타입 체킹과는 다릅니다!) 과정에서 심각한 이슈들을 양산하는 부분이긴하지만, 지금 이 글타래와 큰 상관은 없으니 생략합니다.

Untyped λ-calculus의 나머지 내용은 위와 같은 문법과 의미 정의로부터 출발하는 속성들이므로, 일단은 이 정도만 설명해도 지금 이 글타래에 대한 답변을 진행하는 데에는 충분하지않을까 생각합니다. Typed λ-calculus는 조금 더 재미있어지는데, 지금은 타입 이론까지 자세히 설명할 필요(그리고 시간)가 없을 뿐더러, 무엇보다도 Y combinator가 이슈가 되는 부분은 바로 이것이 untyped λ-calculus의 특징이기 때문이므로 일단 보류하겠습니다.

Combinator란 “함수부에 자유변수가 등장하지 않는 함수”입니다. 즉, 함수부가 오로지 인수들만으로 구성되는 함수라는 뜻입니다. 하지만, 일단은 그냥 위와 같은 람다 텀으로 만들 수 있는 일종의 ‘템플릿 함수’라고 받아들이시면 될 것 같습니다. 물론 Combinatory logic 자체도 일가를 이룬 재미있는 연구 분야이지만, Y combinator의 정체만 간단히 설명하는 데에는 다음과 같은 설명으로 충분할 것 같습니다:

일단, 유명한 SK(I) 시스템을 소개하겠습니다. (단, 앞으로는 불필요한 괄호는 생략합니다. 즉, 람다 텀의 적용은 왼쪽이 먼저 결합하므로 ((L M) N)은 그냥 L M N으로 쓰겠습니다. 또한, 관례적으로 combinator들은 로만체 대문자 볼드로 쓰지만, 이 문서에서는 지금까지처럼 그냥 대문자로 쓰는 것으로만 합니다) SK 시스템이란 말 그대로, S, K 두 개의 combinator들로만 (혹은 조금 사족스럽게 I combintor까지 세개로만) 이루어지는 시스템이고, 이들만 가지고도 대부분(전부 다는 아니고 이게 매우 아스트랄한 부분인데, 저도 당장은 정확히 설명할 수 없으므로 생략합니다. 잇힝~)의 계산을 기술할 수 있는 재미있는 시스템입니다. 각 combinator(즉, 함수)들의 정의는 다음과 같습니다 :

S x y z = x z (y z)
K x y   = x
I x     = x

이 정의가 혹시 juxtapositioning 때문에 헛갈리실까봐, combinatory logic의 관례에는 어긋나지만 (게다가 partial application도 불가능한 다른 타입이 되어버리지만) 편의를 위해 전통적인 표기법으로 다음과 같이 고쳐써보겠습니다:

S(x, y, z) = x(z, y(z))
K(x, y)    = x
I(x)       = x

그런데, 위 정의에 따라 ((S K K) x)를 계산하면 다음과 같습니다:

((S K K) x) = S K K x      -- combinator 적용의 결합 우선순위에 의함
            = K x (K x)    -- S의 정의에 의함
            = x            -- K의 정의에 의함

즉, ((S K K) x) = x입니다. 위에서 I x = x였으므로 결국 I x = (S K K) x가 되고, η-치환 규칙에 따라 (이 η-치환이라는게 좀 문제가 있을 때도 있지만 여기서는 괜찮으니 넘어갑시다) I = S K K입니다. 결론적으로, I의 정의는 위와 같이 따로 정의하는 대신 S와 K의 정의만 가지고도 파생시킬 수 있었다는 얘기입니다. 그래서 이 시스템을 SKI 시스템이라고 하지 않고 SK 시스템이라고 합니다. I와 마찬가지로, 심지어 자연수 체계 같은 대부분의 계산 대상과 함수들(실은 이들이 서로 다르지 않지만)을 오로지 S와 K만으로 나타낼 수 있다는 의미이기도 합니다.

제가 맨 처음에 λ-calculus 이야기를 왜 했냐하면, 사실은 위에 써놓은 S, K, I의 정의는 (λ-calculus의 기본에 비해 상대적으로) 매우 고차원적인 기법인 ‘패턴 매칭’을 이용해 정의한 것이고, 만일 패턴 매칭이 없다면 위에서처럼 정의할 수는 없습니다. λ-calculus의 기본만 가지고 정의하려면 다음과 같이 정의됩니다:

S = λx.(λy.(λz.(x z (y z)))) = λx.λy.λz.(x z (y z))
K = λx.(λy.x) = λx.λy.x
I = λx.x

여기까지는 서론이었고, 이제 본론으로 들어가기 전에 잠깐 (여흥 삼아) 이들 combinator들의 타입을 확인해봅시다. 타입에 대해서 자세히 설명하지는 않겠습니다. (어차피 나중에 Y의 타입을 자세히 들여다봐야하니 여기서는 맛보기만...!) 타입을 제가 그냥 막 써드릴 수도 있지만, 제가 실수할지도 모르니 Haskell 인터프리터의 힘을 잠시 빌려보겠습니다:

Hugs.Base> :type s    where   s x y z = x z (y z)
let {...} in s :: (a -> b -> c) -> (a -> b) -> a -> c
Hugs.Base> :type k    where   k x y = x
let {...} in k :: a -> b -> a
Hugs.Base> :type i    where   i x = x
let {...} in i :: a -> a
Hugs.Base>

이렇게 매우 정상적이고 상식적인 타입들이 나옵니다. (실토하자면, 사실 이 combinator들은 typed λ-calculus의 대표적인 combinator들이었습니다. Typed λ-calculus에서는 예를 들어 Y 같은 (의미상) 말도 안되는 combinator는 만들어질 수도 없고, 만들어져서도 안됩니다. 역사적으로는 오히려 거꾸로, Y 같은 (전통적인 계산학의 테두리 안에서 생각할 때) 허무맹랑한 combinator가 만들어질 수 없게끔 보증하기 위해서 λ-calculus에 type 개념이 추가된 것이라고 보셔도 됩니다.)

자, 그럼 이제 본론인 Y combinator를 보겠습니다. Untyped λ-calculus에 동반하는 combinatory logic에는 전통적으로 수많은 combinator들이 등장했었고 일일이 열거하기도 벅찰만큼 그 종류가 많습니다. 가장 두드러진 예로는 자연수 체계를 combinator로만 표현하는 예가 있으며, 유명한 Church numerals도 (넓은 의미에서는) 일종의 combinator로 볼 수 있습니다. 이 중에서 Y는 일종의 (그리고 가장 대표적인) fixed point combinator입니다. 이미 wikipedia에서 Y의 정의는 찾으셨군요.

토끼군님께서 이미 말씀하신 대로, fixed point란 고정소수점 수를 뜻하는게 아닙니다. 어떤 함수 f의 fixed point란 (혹은 문헌에 따라 줄여서 그냥 fixpoint라고도 하더군요) f(x) = x가 되는 x를 뜻합니다. 이걸 왜 fixed point라고 부르냐하면: ‘일반적’으로 함수는 x, f(x), f(f(x)), f(f(f(x))), ...이렇게 진행될 때마다 그 함수값이 계속 달라집니다만, 만일 어떤 p에 대해서 f(p) = p라면, 이때부터는 f(p), f(f(p)), f(f(f(p))), ... 이렇게 전개해도 더이상 값이 변하지 않고 고정(fix)되기 때문입니다. 자연수를 1 증가시키는 함수 succ을 예로 들면, 0, succ(0), succ(succ(0)), ...가 계속 바뀌다가 ω에 도달하면 더이상 바뀌지 않고 고정됩니다. (ω + 1 = ω) 그래서 succ의 fixpoint는 ω라고 이야기합니다.

λ-calculus로 합성할 수 있는 모든 함수에는 반드시 fixpoint가 있습니다. (Tarski 등을 검색해보셔요~) 이 의미는, 다시 말하자면, 어떤 함수 f를 인수로 주어도 그 함수 f의 fixpoint를 계산해내는 (그 계산 복잡도가 얼마든 간에) 함수 Y가 존재한다는 뜻입니다. 따라서 이런 Y는 반드시 λ-calculus로 만들어낼 수 있습니다. 이게 바로 임창진님께서 이미 찾아내신 표현식
Y = λf.(λx.(f (x x)) λx.(f (x x)))
입니다. 람다 텀으로 써놓으니까 뭔가 무시무시해보이는데, 패턴 매칭을 써서 재귀적으로 정의해도 된다면 다음과 같이 간단히 정의할 수 있게됩니다:
Y f = f (Y f)
(아마 MIT 전산과 홈페이지에 가보면 대문에 그려진 엠블렘에 위 식이 적혀있을겁니다.) 그런데, 눈치채셨을지도 모르지만, 이렇게 정의하면 combinator의 정의에 위배됩니다. Combinator란 분명히 그 함수부에 자유변수가 등장하지 않는다고 했었는데, 위 정의에 보면 Y라는 자유변수(정확한 번역은 아니지만, C 프로그래머가 이해하기 쉽게 약간 외곡해서 번역하자면 global variable)가 등장합니다. 그러니 이렇게 정의한 Y 함수는 함수이긴하되 combinator는 아니죠.

Y는 분명히 combinator이고, combinator답게 S와 K, I만으로 만들어낼 수 있습니다 (단, Untyped라고 가정했을 때에만!):
Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))
(찾으신 wikipedia 문서에 보니 더 간단한 정의도 있군요. 실은 모르고 있었는데, 덕분에 저도 좋은거 하나 알았습니다. :) ) 그런데 이 정의가 과연 타입이 적용되어도 맞을까요? Haskell 인터프리터에게 물어보니:

Comb> :b
module Comb where
s :: (a -> b -> c) -> (a -> b) -> a -> c
k :: a -> b -> a
i :: a -> a
Comb> :type y where y = s (k (s i i)) (s (s (k s) k) (k (s i i)))
ERROR - Type error in application
*** Expression     : s i i
*** Term           : i
*** Type           : (a -> b) -> a -> b
*** Does not match : a -> a -> b
*** Because        : unification would give infinite type

Comb>

라는군요. 역시 안됩니다. 즉, Y라는 놈은 실제로는 ‘최소한 combinator로서는’ 타입이 맞지 않는 괴물딱지죠. 그런데 이런 Y를 일반 함수로는 (당연히) 정의할 수 있습니다. 위에 나왔던 식을 그대로 써보면:

Comb> :type y   where   y f = f (y f)
let {...} in y :: (a -> a) -> a
Comb>

이렇게 되는군요.

왜 Y가 fixed point를 찾아주는지는 위 식을 보시면 곧바로 유추해낼 수 있습니다. 예를 들어 succ이라는 함수를 Y의 인수로 주면:
Y succ = succ (Y succ) = succ (succ (Y succ)) = succ (succ (succ (Y succ)))
이런 식으로 계속 이어집니다. 즉, succ (succ (succ (succ (succ ...., 따라서 자연수의 크기, 즉 ω죠. 그러나, 물론 Y 함수의 의미가 그렇다는 뜻일 뿐이고, 실제로 이 값을 계산해내는건 완전히 다른 이야기입니다.

Comb> (+ 1) 3
4 :: Integer
Comb> y (+ 1) where y f = f (y f)

ERROR - Control stack overflow
Comb>

최대한 간단하게 설명하려고 했는데, 쓰다보니 결국 잡설이 길어져버렸군요. 결론적으로, Lua 코드에 나오는 Y의 정의는 제가 제대로 읽어낼 수 없지만, 아래에 나오는 F의 정의는 대충 읽을만하네요. F는 어떤 함수 f를 입력받아서 새로운 함수 하나를 리턴하는 함수인데, 이 새로운 함수는 자연수 n을 입력받아서 1 혹은 ‘f가 연계된’ 계산값 n * f(n-1)을 리턴합니다. 즉, 이 함수 F의 fixpoint가 곧 factorial 함수가 되는군요.

보너스로 타입을 잠시 추론해보면: F가 리턴하는 함수의 타입은 nat → nat이고, 이 함수의 함수부로부터 f의 타입도 역시 nat → nat이어야함을 알 수 있습니다. 따라서 F의 타입은 ((nat → nat) → (nat → nat))입니다. Y의 타입이 ∀a∈Type: (a → a) → a 이었으므로 이 경우에는 a에 nat → nat이 대응되어 결국 Y의 타입이 ((nat → nat) → (nat → nat)) → (nat → nat)인 셈이고, 따라서 Y(F), 즉 factorial의 타입은 nat → nat이 됩니다.

Y의 정의에서 함수부에 보면 "local"이 아마도 (좀더 널리 쓰이는 용어로) "let"인 모양인데, 그렇게 놓고 보아도 역시 코드가 좀 읽기에 난해하군요. 누군가 Lua를 아시는 분이 답해주시겠죠. 아무튼, 이 Y의 정의가 위에 설명한 Y combinator의 정의를 구현해놓은 것임은 분명합니다:

PS: Y combinator의 경우 (특히 타입 검증을 까다롭게 하는 언어일수록) 실제 계산은 매우 곤란한 문제인데, Lua의 경우에는 Y를 실제로 계산해낼 수 있다는 사실이 매우 흥미롭습니다. 혹은, 제가 결국 읽어내지 못한 저 Lua 코드가 실은 Y combinator의 원래 의미 그대로를 구현해둔 것이 아니라, fixed point에서 정말로 계산을 멈출 수 있게끔 Lua 나름대로의 꽁수를 써서 조금 왜곡해둔 코드인지도 모르죠. 아무튼, 조만간에 Lua를 한 번 제대로 보긴 봐야할 것 같습니다. :)

[/][/][/]

괄호가 틀렸네요. 정확하게 쓰면,
Y = λf.(λx.f (x x)) (λx.f (x x))

그리고 Y combinator도 recursive type으로 타입을 입힐수 있습니다.
ocaml에서,

$ ocaml -rectypes

# let y f = (fun x -> f (x x)) (fun x -> f (x x));;
val y : ('a -> 'a) -> 'a = <fun>

ocaml이나 lisp처럼 eager evaluation을 하는 대부분의 언어들은 Y combinator를 쓰면 combinator 자체 계산에서 무한 loop에 빠집니다. 그래서 약간 다른 형태의 Y combinator를 이용합니다. 위의 lua 예제도 아래 Y'을 이용했습니다.

Y' = λf.(λg.λx.f (g g) x) (λg.λx.f (g g) x)

$ocaml -rectypes

# let y' f = (fun g -> fun x -> f (g g) x) (fun g -> fun x -> f (g g) x);;
val y' : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# (y' (fun f -> fun n -> if n=0 then 1 else f (n-1) * n)) 5;;
- : int = 120;;

recursive type(mu-type)은 functional 쪽보다는 oo 쪽에서 더 중요합니다.(object의 self type) 그래서 ocaml(objective caml)은 지원하지만 haskell은 제낀듯하군요;;;

정정사항: Y combinator자체의 계산에서 무한루프에 빠지는 것이 아니라 Y f, 즉 함수의 fixed point를 구하는 과정에서 무한루프에 빠집니다.

헉! 역시 변형된 Y였군요.

그나저나 (아무리 자주 손대지는 않는다고 해도) 저도 Ocaml을 계속 보고 있다고 생각하고 있었는데, 제일 중요한 포인트 하나를 이렇게 놓치고 있었군요. 이런 중요한 사실을 오늘에야 처음 알게되었다니, 충격입니다. OTL

답변 달러 들어왔다가 오히려 제가 많이 배우고 갑니다. :)

ω과 자연수의 집합 N과 달라야 하는 이유를 알 수 있을까요?
일단 이 부분을 제가 작성할 때 제가 생각했던 바를 말씀드리자면
ω는 peano axiom을 만족하는 집합이고 따라서 그것을 만족하도록 ω = {0} U { succ(n) | n은 ω의 원소 }를 만족하는 최소크기의 집합으로 정의를 한 것입니다.
즉 이 부분에서는 저는 단지 ω를 peano axiom을 만족하는 집합으로 보았습니다.

여기서부터는 아래 말씀하신대로 ω가 전통적인 집합론에서 말하는 것으로 생각하겠습니다.

어떻게 ω = φ ∪ { ω }이란 식을 얻으셨는지 궁금합니다.
아마도 자연수들의 집합인 ω 자체를 하나의 수라고 볼 때(즉 ordinal),
ω가 limit ordinal임을 생각하지 않으신 것 같습니다(즉, "ω는 어떤 수의 successor도 아니다"라는 것)

사실 저는 그런 의도로 F를 정의하지 않았는데도 이렇게도 해석이 가능하네요(신기하네요 :))
저는 단지 자연수의 집합 ω가 어떤 함수의 fixpoint로 정의(표현) 가능하다는 것을 보여주고 싶었을 뿐입니다.
위에서와 같이 "X+1 = X U {X}이다"라는 집합론적 자연수의 정의를 전혀 가정하지 않고
자연수의 집합 ω는 ω = {0} ∪ { succ(n) | n ∈ ω }를 만족하는 최소의 집합이라는 것으로부터
마치 이 쓰레드의 원래 주제인 :) 재귀함수를 Y combinator를 이용한 비재귀함수로 바꾸는 것과 비슷한 테크닉으로
오른쪽 term에 나타나는 ω를 어떤 인자 X로 치환시켜서 얻은 것입니다.
즉 F = \X. {0} ∪ { succ(n) | n ∈ X }
그런 후에 마치 저 위의 쓰레드 글에서와 같이 fact = Y F (여기서 F = \f.\n.if n=0 then 1 else n*f(n-1)) 인 것과 비슷하게
ω = least fixpoint of F (여기서 F = \X. {0} ∪ { succ(n) | n ∈ X } )를 얻은 것입니다.
F(φ) = {0}
F({0}) = {0, succ(0)}
F({0,succ(0)}) = {0, succ(0), succ(succ(0)) }
.....
F(ω) = ω

즉 제가 F를 정의할 때의 의도는 F의 정의에서 보이는 그대로
어떤 자연수들의 집합 X를 받아들여서 0과 X의 각 자연수들의 successor들의 집합을 반환해 주는
특별한 의미가 없는 함수로 정의하였습니다.

네.. 잘못 생각하고 계시는 것 같습니다.
일단 제가 말한 '가장 큰 원소'는 greatest element를 말한 것입니다.
ω가 LUB는 있어야 할 것 같다고 하셨는데 물론 유한한 집합에 대해서는 LUB가 존재합니다.
예를 들면 {1,4,5,7}과 같은 집합의 LUB는 7이 되겠지요.
하지만 짝수집합과 같은 무한한 집합에 대해서는 LUB가 존재하지 않습니다.
LUB가 ω가 되지 않느냐고 하셨는데 그렇지 않습니다.
LUB라는 것은 여전히 그 원소자체도 우리가 대상으로 하고 있는 집합에 속해야 하기 때문입니다.
즉 차리서님의 말씀대로라면 ω∈ω가 되어버리는 것입니다.
그런데 이것은 사실이 아니죠.

ω와 N 모두 자연수들의 집합을 의미하기 때문에 서로 같은 것으로 생각하겠습니다.
결론은 ω\∈ω 입니다.
자연수들의 집합인 ω 자체가 자연수가 아니라는 사실을 생각하시면 됩니다.
왜 ω자체가 자연수가 아닌지는 ω가 어떤 자연수의 successor도 아니라는 사실로부터 입니다(즉 limit ordinal).
(자연수이려면 0이거나 혹은 어떤 자연수의 successor이어야 합니다)

잠시 안들어오고 있는 사이에 이런 주제가 이야기 되고 있었네요
아직 다 읽어보질 못해서 잘 모르지만.

LUB 가 제가 아는 Least Upper Bound 라면 대상 집합에 항상 속해 있어야 합니다. 제가본 정의에선 대상 집합에 속해 있게 정의가 되어 있습니다.

다시 보니 대상 집합을 s,t 라고 보면 속해있지 않아도 되는군요~
여기서 대상 집합의 정의가 어떻게 되는거죠??