#Scala/Chapter0#

Lambda Calculus

lambda之所有这么重要，是因为它具有“二象性”：它既可以被看作一种简单地程序设计语言，用于描述计算过程；也可以被看做一个数学对象，用于推导证明一些命题。

Function (函数)

Black Box
Pure
我们把函数看成一个Black Box，x -> f -> y 就是只有一个输入和对于同一个输入只产生唯一一种结果。也就是说输出 y 只依赖于输入 x ，并无其他任何因素可以影响函数的输出结果 y。

Functional Model of Computation

Express computation based on
- (anonymous ) function ~abstraction~ and
- function ~application~ via binding and substitution
  function abstraction 函数抽象指的是用lambda表示的式子
  function application 指的是lambda式子右边的值带入左边的lambda式子里面替换式子的 body 里面与变量绑定的值。
Equivalent to state-based Turing Machine by Alan Turing

Syntax

lambda expressions are :

E = ID for example : x,y,z,…..variables ID
E = /ID. M the abstraction symbols lambda ‘/’ and dot ‘.’
E = (MN) parentheses ()
E = (E)
pure lambda calculus does not define constants, operators, etc.

便于理解的例子 & Currying

平方和函数：f(x,y) = x*x + y*y | f(3,4) = 3*3 + 4*4
映射： (x,y) -> x*x +y*y | ((x,y) -> x*x +y*y)(3,4) = 3*3 + 4*4
变一下形式，编程单参数函数:
(x -> (y -> x*x + y*y)) 什么意思呢，把x 映射为另外一个y的映射~ (x -> (y -> x*x + y*y))(3) = (y -> 3*3 + y*y)
(y -> 3*3 + y*y)(4) = 3*3 + 4*4
这样子就把 f(x,y) 变成了 f(x)(y) 用类似的方法把多个参数的函数编程单个参数的函数的高阶函数，这个转换叫做 currying。
更易于理解的看一下：
def f(x:Int,y:Int):Int = x*x +y*y变成了：

1
2
3

def f(x:Int):Int = {
	def f(y:Int):Int = x*x + y*y
}

以上都是我个人理解，代码不准确，想表达某一个意思呢，我也不知道怎么说好，第一上面的应该是匿名函数，我写成了有名字的函数呢。然后。。。

为什么要转换？意义是什么？

Notation Simplification(符号简化)

lambda 式子中的最外层的括号可以摘掉例如 (/x.x) -> /x.x
lambda 式子是左结合的，所以是左面优先的例如 (((MN)P)Q) -> MNPQ

Disambiguation Rules(不暧昧规则)

Application are assumed to be left associative :
- M N P my be written instead of ((MN)P)
The body of an abstraction extends as far as possible:
- /x.MN are not (/x.M)N , they are different
- (/x./y.yx)ab != /x./y.yxab
- ((/x./y.yx)ab) and (/x./y.(yxab))
/x.AB means /x.(AB) is an function abstraction while
(/x.A)B is an function application means B is a parameter of
the function (/x.A)

Abstraction Syntax Tree

lambda: abstraction operator
apply: application operator

the right subtree of the apply node is the actual argument
the left subtree of the apply node is (with a lambda at its root) the function
the left child of the lambda is the _ parameter.
the right child of the lambda is the function body.

Problems with the naive rewriting rule

Simple rule for rewriting (/x.M)Nmeans “replace all occurrences of x in M with N”. However , there are two problems with this rule

“Scope escape” problem
“Capture” or “name clash” problem

Problem 1 : Scope escape :

 (/x.(x + ((/x.x+1)3)))2 
=> (/x.(x+(3+1)))2
=> (/x.(x+4))2
=> (2+4) => 6
--------------------------------------------------------------
 (/x.(x + ((/x.x+1)3)))2
=> (2+ ((/x.2+1)3)) )
=> (2+ (2+1))
=> (2+3) => 5

也就是这里的第一个x 绑定的是最外层的x 而最内层的x 绑定的则是内部的x 他俩绑定的值不一样所以用最外层2 带入值的时候不可以替换内部的呢，所以会出现问题。

Problem 2 : Name clash :

((/x./y.x)y)z
=> (/y.y)z
=> z
----------------
((/x./a.x)y)z
=>(/a.y)z
=> y

本来的y 和 /y 没有绑定关系的，但是在带入之后突然就有了关系，这样就造成了错误的绑定和错误的结果。

Bound & Free Variables

Bound Variable：a variable that is associated with some lambda
Free Variable：a variable that is not associated with any lambda
Intuitively , in lambda-expression M, variable x is bound if , in the AST, x is in the subtree of a lambda with left child x. 这句话换句话就是如果这个 x 是处于 lambda Scope 范围内的话他就是被 lambda 绑定的变量，除非里面没有另一个 lambda x 式子。

FV(x) = {x}
In the expression x , variable x is free. 因为没有lambda 单独的x 当然是free
FV(M,N) = FV(M) U FV(N)
In the expression M N :
a. The free variables of M N are the union of two sets.
b. The bound variables of M N are also the union of two sets.
FV(/x.M) = FV(M) - {x} (除了x M中的自由变量都是自由的)
In the expression /x.M,
every x in M is bound;
Every variable y != x that is free in M is free in /x.M;
Every variable is bound in M is bound in /x.M.

练习：

1	(/x. x(/y.xyzy)x )xy

Solution of the Problem 1 :

Revised Rewriting Rule : To solve this problem ,given lambda expression
(/x.M)N “Replacing all occurrences of x that are free in M with N”
(/x. x + ((/x.x +1)3)) 2
这里的第一个 x 是 M 中的 free 变量，而第二个里面的 x 则是在 M中有绑定值。所以我们可以在 application的时候用2 来替换 M中的第一个free的变量x 。这里的x 对于 M来说是 free 但是对于 lambda 表达式来说是 bounded。
(/x. x + ((/x.x +1)3)) 2 => 2+((/x.x +1)3)

Solution of the Problem 2:

The variable y that is free in the argument to a lambda expression becomes bounded after rewriting , because it is put into the scope of a lambda expression with a formal parameter named y:
((/x./y.x)y)z这里的外层的y 进入内层替换x 之后就变得绑定了。所以引出了阿尔法等式：

a-equivalence (a 等价) & a-conversion (a 约定)

The basic idea is that formal parameter names are unimportant ;so rename them as needed to avoid capture or name clash.
a-conversion modifies expressions of the form /x.M to /z.M
rename all the occurrences of x that are free in M to some other variable z that does not occur in M (and then /x is changed to /z).意思就是 M中的free的x 才是 /x.M 中和 lambda 绑定的x 而 M 中 bounded的 x 则是内部绑定的和外部的 lambda 没有绑定关系所以不能替换，所以先把外部的 /x. 替换成 /z.把 M中 free的 x 替换成z. 注意的是 z 不允许出现在 M中反而产生别的问题。
/x./y.x+y可以通过 a-reduces 到 /z./y.z+y

Renaming Operation (a-conversion)

E{y/x} 用 y 替换 x
- x{y/x} = y
- z{y/x} = z, if z!= x
- (M N){y/x} = (M{y/x})(N{y/x})
- (/x.E){y/x} = (/y.E{y/x}) if no y in E 
- (/z.E){y/x} = (/z.E{y/x}) if z != x
example :
((/x.x(/y.xyzy)x) x y){bar/x}
----------------  - - 
		A 		    B C
=> (/x.x(/y.xyzy)x){bar/x}(x){bar/x}(y){bar/x}
=> (/bar.(x(/y.xyzy)x){bar/x}) bar y
=> (/bar.bar (/y.xyzy){bar/x} bar) bar y
=> (/bar.bar (/y.bar yzy)bar) bar y

a-equivalence

For all expressions E and all variables y that do not occur in E
/x.E =a /y.(E{y/x})

Substitution (替换)

substitution 的目的是把M中的自由变量x (也就是受/x 约束的 x 替换成 N实现application)
(/x.+x1)2 -> (+ 2 1) replace a variable by a lambda expression

E[ x -> N ] ，when E and N are lambda expressions and x is a name.

(/y./x.yx)(/z.xz)
=>(/x.yx)[y -> /z.xz]
=>(/x.(/z.xz)x) => trouble! 
因为 /z.xz 中的 x 本来是 自由变量而在替换之后和里面的 /x 产生bound关系了，所以在替换前对于原来的式子使用 a-reduction! 
=> (/w.(/z.xz)w)这样就没有多添加的关系了。

Substitution Rule

E[x->N]
1. x[x->N] = N
2. y[x->N] = y, if x != y
3. (E1 E2)[x->N] = (E1[x->N])(E2[x->N])
4. (/x.E)[x->N] = (/x.E) 里面不可能有 free 的 x ！！这个要想一下
5. (/y.E)[x->N] = (/y.E[x->N])when y!= x and y不属于FV(N)如果N中存在free的 y 那么替换之后 会突然增加绑定关系
6. (/y.E)[x->N] = (/z.E{z/y}[x->N])when y != x and y 属于 FV(N) 								   and z != x and z 不属于 FV(N) 
sepecial : 4条 有点模糊哦，
(/x.E)[x->N] 意味着 (/x./x.E)(N) 这种情况要带入N 然后替换 /x.E 中和 外部的/x 绑定的 x 但是 /x.E 中肯定不可能存在和外部绑定的x 都被里面的/x所绑定了。所以  (/x./x.E)(N) = /x.E 所以才有的 (/x.E)[x->N] = (/x.E)

Example :

(/x.x)[x->foo] => /x.x  by (4)
(+1x)[x->2]
=> (+[x->2] 1[x->2] x[x->2]) by(3)
=> (+ 1 2) by (2),(1)
--------------------------------------------------------------
(/y./x.yx)(/z.xz)
(/x.yx)[y->/z.xz]
=> (/w.yw)[y->/z.xz]  by(6) since x 属于 FV(/z.xz)
=> (/w.(yw)[y->/z.xz])   by (5)
=> (/w.(y[y->/z.xz] w[y->/z.xz])) by (3)
=> (/w.(/z.xz) w) by(1),(2)
--------------------------------------------------------------
(/x./y.(/f.fx)y)(fy)
(/y.(/f.fx)y)[x->fy]
=> (/w.(/f.fx)w)[x->fy]  by(6) since y 属于 FV(fy)
=> (/w.(/f.fx)[x->fy]w[x->fy]) by(5),(3)
=> (/w.(/f.fx){f/z}[x->fy] w) by(6),(2) since f 属于 FV(fy)
=> (/w.(/z.zx)[x->fy] w )
=>  /w. (z(fy)) w 
--------------------------------------------------------------
(/y./z.yz)(/z.xz)
(/z.yz)[y->/z.xz]
=> (/z.(yz)[y->/z.xz])
=> (/z.(y[y->/z.xz] z[y->/z.xz]) )
=> /z.( (/z.xz) z )

Precise Meaning of Rewriting : Beta-reduction

进行Substitution 的过程叫做 B-reduction
(/x.M)N -> B M[x -> N]
左边的部分(/x.M)N 叫做 redex(可约式)
右边的部分 M[x -> N] 叫做 contractum (缩减项)
中间的 -> B 记号(notation)意味着 all free occurrences of x replaced with N in a way that avoids capture/Name clash .
个人想法：这是种什么感觉呢就是比如一个f(x)(y) ，f(3)通过一次Beta-reduction 把x相关的都用 3 替代了。然后计算 y 部分的。或者说
(/x./y.E)N 然后通过B-reduction 把跟 /x 相关的绑定变量都用N替代了。接下来就编程了只有一个参数y的函数了。

Normal Form (范式)

A computation is finished when there are no more redexes.
A lambda expression without redexes is in normal form.
A lambda expression has a normal form iff there is some sequence of B-reduction that leads to a normal form.

Ps: 不是所有的式子都可能 B-reduce到 Normal form ，因为有些式子越约越长。。
如果你得到一个B范式，那么可以确定他是唯一的，不用担心因为规约顺序而导致不同的结果，换句话说一个式子不论怎么规约，只可能规约出唯一的一种范式。

(/x.x)y 
=> x[x->y]
=> y
------------
(/x.x(/x.x))(ur)
=>(x(/x.x))[x->ur]
=>x[x->ur](/x.x)[x->ur]
=>ur(/x.x)
-----------------------
(/x.y) ((/z.zz)(/w.w))
------ ---------------
  A           B
=> (/x.y) (zz)[z->/w.w]
=> (/x.y) ((/w.w)(/w.w))
=> (/x.y) (w)[w->/w.w]
=> (/x.y) (/w.w)
=> (y)[x->/w.w]
=>  y
另一种顺序的算法：
(/x.y) ((/z.zz)(/w.w))
------ ---------------
  A           B
=> (/x.y)[x->((/z.zz)(/w.w))]
=> y

Yita-Reduction

if v is a variable , E is a lambda expression (denoting a function), and v has no free occurrence in E,
/v.(Ev) =>yita E

/x.(sqr x) =>yita sqr
/x.(add 5 x) =>yita (add 5)

The yita-reduction rule can be used to justify the extensionality of functions; namely, if f(x) = g(x) for all x, then f = g.

理解的不多，就是比如说哦 (/x.fx)y=>fy ,所以是不是感觉到了 (/x.fx) = f 在某种意义上。但是如果 f 中存在着 x 的自由变量，那么意味着这个f 中的自由变量x 是和外面的 /x 绑定的，那么就是说 f 会在 y 导入的时候发生变化的。那么久不一定相等了，所以才有的这么一个条件就是在 E 中不存在 v 的自由变量的时
候 /v.(Ev) =yita E

deta-reduction

if lambda calculus has predefined constants(that is , if it is not pure),rules associated with those predefined values and functions are called deta-rules.
for example:
(add 3 5) =>deta 8 ,
(not ture)=>deta flase.

Pure Lambda Calculus

这里想说的核心内容就是： Booleans, integers, and (other data structures) can be entirely replaced by functions!!!

Branch

if p then q else r can be thought as COND p q r

TRUE x y -> x
FALSE x y -> y
Then COND = /p./q./r.p q rwhere
TRUE = /x./y.x FALSE = /x./y.y

COND TRUE a b 记住了lambda简化必须是左结合
=> (/p./q./r.pqr)(/x./y.x)ab
=> (/q./r.(/x./y.x)qr)ab
=> (/x./y.x)ab
=> a

Boolean Logic

TRUE = /x./y.x
FALSE = /x./y.y
AND = /a./b. a b FALSE
OR = /a./b. a TRUE b
NOT = /a.a FALSE TRUE

and T F
(/a./b. a b (/x./y.y))(/x./y.x)(/x./y.y)
=> (/x./y.x)(/x./y.y)(/x./y.y)
=> (/y.(/x./y.y))(/x./y.y)
=> (/x./y.y)
=> F
--------------------------------------------------------------
not TRUE
(/a.a FALSE TRUE)TURE
=> (TURE FALSE TRUE)
=> FALSE

Functional programming in Scala(0)