最近試用pure λ Calculus喺Haskell度砌啲基本嘢...

1. 用Church numerals砌natural numbers
Zero = λ s z . z
One = λ s z . s z
Two = λ s z . s (s z)
Three = λ s z . s (s (s z))
(where s = successor, z = zero)




2. 跟住砌埋arithmetic add operator e.g add x and y
add = λ s z x y . x s (y s z)



3. 然後用Church Boolean砌logical and/or/not operators
TRUE = λ t f . t
FALSE = λ t f . f

And = λ x y . x y FALSE
Or = λ x y. x TRUE y
Not = λ x . x FALSE TRUE



Conclusion: 阿Church真係CLS, 簡真天才嚟, 佢點諗到架?!!!

(BTW, 學λ Calculus基本上只需要明白α-conversion(用嚟avoid namespace collision between different functions)同β-reduction(用嚟do computation)呢兩個簡單operations,加上知道下lazy evaluation係左去右(唔同平時見慣嘅右去左eager evaluation)就OK了, 唔算好複雜, 比mathematical Differential Calculus淺好多好多! )

順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

ok睇唔明

順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

下面解釋番Yf變成fYf嘅steps:
1) Y combinator defined:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
2) Application of Y combinator on function f:
Y f = ( λ y . ( λ x . y (x x)) ( λ x . y (x x))) f
3) β-reduction:
Y f = ( λ x . f (x x)) ( λ x . f (x x))
4) β-reduction again:
Y f = f ( λ x . f (x x)) ( λ x . f (x x))
5) As shown in step 3 above, Y f = ( λ x . f (x x)) ( λ x . f (x x)), so:
Y f = f Y f

ok睇唔明

各大definitions(i.e. Church numerals, Church booleans, add, and/or/not, Y combinator, etc.)係Alonzo Church呢位天才諗出嚟, 我都只係抄出嚟放落Haskell用咁啫, 唔明我都冇辦法!

順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

純lambda calculus係唔type嘅。Haskell有type system限制(Hindley Milner type system唔能夠代表到y combinator嘅type），唔可以寫到純lambda calculus嘅y combinator。

http://stackoverflow.com/questions/4273413/y-combinator-in-haskell

Haskell嘅fixed point operator叫fix

GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Data.Function
Prelude Data.Function> :t fix
fix :: (a -> a) -> a
Prelude Data.Function> let fact f n = if n == 0 then 1 else n * f (n - 1)
Prelude Data.Function> :t fix fact
fix fact :: (Eq a, Num a) => a -> a
Prelude Data.Function> fix fact 5
120
Prelude Data.Function> map (fix fact) [0..10]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]
Prelude Data.Function> let y f = f (y f) -- not really the y combinator
Prelude Data.Function> :type y
y :: (t -> t) -> t
Prelude Data.Function> y fact 5
120
Prelude Data.Function> map (y fact) [0..10]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]
Prelude Data.Function>


我以前響高登講過點用lisp寫y combinator。不過因為strict evaluation關係，同pure lambda calculus都係有dd分別。

http://forum14.hkgolden.com/view.aspx?type=SW&message=5112005&highlight_id=0&page=2&authorOnly=False

順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

純lambda calculus係唔type嘅。Haskell有type system限制(Hindley Milner type system唔能夠代表到y combinator嘅type），唔可以寫到純lambda calculus嘅y combinator。

http://stackoverflow.com/questions/4273413/y-combinator-in-haskell

Haskell嘅fixed point operator叫fix

GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Data.Function
Prelude Data.Function> :t fix
fix :: (a -> a) -> a
Prelude Data.Function> let fact f n = if n == 0 then 1 else n * f (n - 1)
Prelude Data.Function> :t fix fact
fix fact :: (Eq a, Num a) => a -> a
Prelude Data.Function> fix fact 5
120
Prelude Data.Function> map (fix fact) [0..10]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]
Prelude Data.Function> let y f = f (y f) -- not really the y combinator
Prelude Data.Function> :type y
y :: (t -> t) -> t
Prelude Data.Function> y fact 5
120
Prelude Data.Function> map (y fact) [0..10]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]
Prelude Data.Function>


我以前響高登講過點用lisp寫y combinator。不過因為strict evaluation關係，同pure lambda calculus都係有dd分別。

http://forum14.hkgolden.com/view.aspx?type=SW&message=5112005&highlight_id=0&page=2&authorOnly=False

明白哂, 咁即係Haskell冇純Y combinator嗰隻type, 唯有用番Data.Function library裏面個fix operator嚟攪, 或者偷雞用let y f = f (y f) 算數, 總之就冇得自己define個真真正正嘅Y combinator啦!

順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

純lambda calculus係唔type嘅。Haskell有type system限制(Hindley Milner type system唔能夠代表到y combinator嘅type），唔可以寫到純lambda calculus嘅y combinator。

http://stackoverflow.com/questions/4273413/y-combinator-in-haskell

Haskell嘅fixed point operator叫fix

GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Data.Function
Prelude Data.Function> :t fix
fix :: (a -> a) -> a
Prelude Data.Function> let fact f n = if n == 0 then 1 else n * f (n - 1)
Prelude Data.Function> :t fix fact
fix fact :: (Eq a, Num a) => a -> a
Prelude Data.Function> fix fact 5
120
Prelude Data.Function> map (fix fact) [0..10]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]
Prelude Data.Function> let y f = f (y f) -- not really the y combinator
Prelude Data.Function> :type y
y :: (t -> t) -> t
Prelude Data.Function> y fact 5
120
Prelude Data.Function> map (y fact) [0..10]
[1,1,2,6,24,120,720,5040,40320,362880,3628800]
Prelude Data.Function>


我以前響高登講過點用lisp寫y combinator。不過因為strict evaluation關係，同pure lambda calculus都係有dd分別。

http://forum14.hkgolden.com/view.aspx?type=SW&message=5112005&highlight_id=0&page=2&authorOnly=False

明白哂, 咁即係Haskell冇純Y combinator嗰隻type, 唯有用番Data.Function library裏面個fix operator嚟攪, 或者偷雞用let y f = f (y f) 算數, 總之就冇得自己define個真真正正嘅Y combinator啦!

I think fix is defined as fix f = f (fix f) in the library. This is purely Haskell magic that you can defined a fixed point operator so easily.

ok睇唔明

lambda calculus係一個電腦嘅數學模型以數學嘅函數（function）做基礎，另一個電腦嘅數學模型係Turing machine。建立數學模型其中目的係決定有乜嘢係電腦可以解決嘅問題。

lambda calculus睇嚟好簡單但已經可以解決任何目前任何電腦可以解決嘅問題，但解決方法可以好低效率。整數運算係一個常見嘅問題，一般電腦可以做，咁用lambda calculus點做呢？首先我地要以lambda calculus嚟表達數目。Church numerals就係一種用lambda expression encode正整數嘅方法。因為lambda calculus裡面除function外乜都無，我地就用function嘅特性嚟代表數目。

function composition：

apply = λ f . (λ x . f x)

apply 係一個function，如果你俾一個function f，apply會俾返另一個function去call f。因為lambda calculus乜Q都係function，所以所以function都係high order。

apply-2 = λ f . (λ x . f (f x))

apply-2 係一個function，如果你俾一個function f，apply-2會俾返另一個function去連續call f兩次。呢個有叫function composition。

apply-3 = λ f . (λ x . (f (f (f x))))

apply-3 係一個function，如果你俾一個function f，apply-3會俾返另一個function去call f 三次。

於此類推apply-n 係一個function，如果你俾一個function f，apply-n會俾返另一個function去call f n次。Church encoding就係用apply-n去代表正整數n

;; identity function.

id = λ x . x

;; if you compose a function zero time, you are not calling it.
0 = λ f . id
1 = λ f . (λ x . f x)
2 = λ f . (λ x . f (f x))
3 = λ f . (λ x . f (f (f x)))
4 = λ f . (λ x . f (f (f (f x))))
....

successor:

我地有正整數，但淨得數目無乜用。我地要諗下點樣可以用數目嚟運算。例如簡單搵下一個數目。

succ = λ n . (λ f . (λ x . (f ((n f) x))))

因為 (n f) x = f(f(f(... f x)，compose f 次。所以 (f ((n f) x))就係將f compose n+1次

addition:

3 + 2 = (1 + (1 + (1 + 2)))
= succ(succ(succ(2))

add = λ m . (λ n . ((m succ) n))

上次C4F巴打講完, 我都去刨左果篇PAPER, 諗法幾得意
雖然一手計就寫到手軟

multiplication:
我地可以當Church numerals係一般數目，咁乘法可以咁做：

2 * 3 = (((0 + 2) + 2) + 2)

mul = (λ m . (λ n . (n (λ x . ((add m) x))) 0))

但如果考慮埋Church numeral同function composition嘅關係，可以聰明D：

mul = (λ m . (λ n . (λ f . (m (n f)))))

上次C4F巴打講完, 我都去刨左果篇PAPER, 諗法幾得意
雖然一手計就寫到手軟

You can read a whole book on this for free made available by its author:

http://www.macs.hw.ac.uk/~greg/books/

完全唔明

建議你裝Haskell嚟試學functional programming, 習慣咗個syntax後先睇番Lambda Calculus, 咁你會明白好多!

P.S. 過來人經驗之談!

multiplication:
我地可以當Church numerals係一般數目，咁乘法可以咁做：

2 * 3 = (((0 + 2) + 2) + 2)

mul = (λ m . (λ n . (n (λ x . ((add m) x))) 0))

但如果考慮埋Church numeral同function composition嘅關係，可以聰明D：

mul = (λ m . (λ n . (λ f . (m (n f)))))

順手砌埋arithmetic mul operator e.g. multiply x and y

mul = λ x y s . x (y s)

multiplication:
我地可以當Church numerals係一般數目，咁乘法可以咁做：

2 * 3 = (((0 + 2) + 2) + 2)

mul = (λ m . (λ n . (n (λ x . ((add m) x))) 0))

但如果考慮埋Church numeral同function composition嘅關係，可以聰明D：

mul = (λ m . (λ n . (λ f . (m (n f)))))

順手砌埋arithmetic mul operator e.g. multiply x and y

mul = λ x y s . x (y s)

上面嗰個有點兒簡化咗, 改成下面咁樣會好啲

mul = λ x y s z . x (y s) z

有加有乘，減數點做？

有加有乘，減數點做？

睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/後放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!

有加有乘，減數點做？

睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/後放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!

其實唔難。Church numerals只可以代表自然數。3 - 5 係無辦法減到。但你可以用sign and magnitude代表整數，用一個boolean加一個Church numeral。

先定義自然數減法natsub:

-- this is Haskell, not λ calculus
natsub m n = if m >= n then m - n else 0

整數減法可以用natsub嚟implement，假設m，n都唔係負數：

sub m n = if natsub m n >= 0 then natsub m n else -(natsub n m)

其他三個case差唔多處理。

響 λ calculus，natsub可以咁定義：

natsub = λ m . λ n . n pred m

pred係predecessor，之前一個數。因為0無predecessor，我地定pred 0 做 0

要定義pred，我地可以用record type幫手。

pair:

-- form an ordered pair
pair = λ x . λ y . λ f . f x y

e.g. pair 0 3 = λ f . f 0 3

-- read first and second elements of a pair
fst = λ p . p true
snd = λ p . p false

記得
true = λ t . λ f . t
false = λ t . λ f . f

有pair就可以寫pred，方法係pipelining。

-- (x, _) -> (succ x, x). The second element always lag behind the first if
-- pre_step called more than 0 times.
pred_step = λ p . pair (succ (fst p)) (fst p)

pred = λ n . snd (n pred_step (pair 0 0))

有加有乘，減數點做？

睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/後放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!

哈，呢篇野嘅方法基本上同我嘅係一樣。

有啲似睇緊abstract algebra啲嘢

有加有乘，減數點做？

睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/後放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!

哈，呢篇野嘅方法基本上同我嘅係一樣。

但我lap一lap你整pred嗰啲steps, 好似仲易明過呢篇嘢喎, 正!