1.0. Lời tựa

Ý tưởng của giải tích $\lambda$ thực ra rất đơn giản và cơ bản. Khi dùng giải tích $\lambda$, chúng ta sẽ mã hóa (encode) mọi thứ khả lập trình (programmable) như if-else clause, while-loop clause hoặc thậm chí là cả True-False.

Đối tượng được sử dụng để biểu diễn là các hàm, được kí hiệu là $f$. Hàm ở đây vẫn là các hàm thông thường, tức là nó có khả năng nhận input, xử lý input và cuối cùng trả về output nào đó. Tuy nhiên, lưu ý rằng các hàm khi được sử dụng trong toán sẽ là hàm thuần túy (pure function) và có một số khác biệt so với hàm trong lập trình như sau:

(1) Là black-box: tức là chúng ta không biết được cụ thể các bước tính toán ở trong hàm, chỉ biết được công dụng của hàm là gì, hoặc thậm chí trong một số trường hợp có thể không biết luôn.

(2) Không có side-effect: khi đưa input vào $f$, $f$ không tác động gì đến đối tượng đó, hay nói dễ hiểu hơn là $f$ sẽ tạo ra phiên bản copy của input khi tính toán và cuối cùng đào thải phiên bản copy đó khi tính toán xong.

(3) Không có internal state: đây là điểm khác biệt khi so sánh mô hình giải tích $\lambda$ của Church với máy Turing của Alan Turing, tất cả đối tượng trong giải tích $\lambda$ đều không thay đổi tại tất cả thời điểm (hết sức thuần túy và đơn giản). Trong khi đó với máy Turing, tại mỗi thời điểm $t$, reader và tape sẽ ở một trạng thái nào đó có khả năng khác với ban đầu.

1.1. Cú pháp

Xét một hàm cơ bản là hàm hằng, tức $f(x)=x$. Hàm này sẽ trả về mọi thứ nó nhận vào mà không tính toán gì cả. Khi chúng ta sử dụng giải tích $\lambda$, $f$ được viết lại theo một số bước như sau.

B1. Bỏ bớt các dấu ngoặc

\[f x = x\]

B2. Tổng quát hóa kí hiệu cho các hàm và thay dấu ‘=’ bằng dấu ‘.’. Đặt trường hợp chúng ta xử lý nhiều hàm cùng lúc, thay vì kí hiệu là $f_1,f_2,…$, chúng ta sẽ kí hiệu chung là dấu $\lambda$. Thực ra kí hiệu này có nhiều ý nghĩa hơn là việc thay thế, các bạn sẽ thấy rõ hơn ở các ví dụ dưới.

\[\lambda x.x\]

Ví dụ với một số hàm khác, như hàm increment: $\lambda x.x+1$, hay hàm add $\lambda x.\lambda y.x+y$

Tóm tắt lại, trong giải tích lambda, chúng ta sẽ gọi chung tất cả các đối tượng là biểu thức lambda (lambda term), nếu chi tiết hóa, các biểu thức lambda sẽ bao gồm:

  • x, y, z (biến - variable): đại diện cho tham số truyền vào hàm. Biến ở đây có thể là các giá trị nguyên thủy (primitive) hoặc do chúng ta tự định nghĩa, hoặc tổng quát hơn có thể là các hàm và biểu thức $\lambda$ khác. Nói chung nó có thể là bất cứ thứ gì.

  • $M = \lambda x.y$ (hàm - abstraction): đây là định nghĩa cho một hàm nào đó, như ta đã thấy. x như ta đã biết được gọi là biến hoặc bound variable. y ở đây cũng có thể là bất cứ thứ gì.

  • $M\;N$ (phép ánh xạ / áp dụng - application): ánh xạ một hàm lên một biểu thức lambda nào đó, trong lập trình thì chúng ta hay gọi là phép gọi hàm.

1.2. Reduction

Chúng ta có 2 phép biến đối sau trong quá trình viết các biểu thức lambda.

$\alpha$-conversion: $\lambda x.M[x]\rightarrow\lambda y.M[y]$. Đơn giản là phép đổi tên biến, chúng ta sử dụng trong trường hợp các biến trùng tên nhau.

$\beta$-reduction: $(\lambda x.M) E\rightarrow M [x:=E]$, khi ánh xạ hàm lên một biểu thức nào đó, chúng ta có thể kí hiệu rõ ràng như vậy.

1.3. Ví dụ

Giả sử chúng ta có hàm add $\lambda x.\lambda y. x+y$.

Chúng ta đã biết hàm add có thể ánh xạ lên một cặp số để trả về kết quả là tổng cặp số đó.

$(\lambda x.\lambda y. x+y)(1,3) = 4$ hoặc $(\lambda x.\lambda y. x+y)\;1\;3 = 4$

Sự ảo diệu của giải tích lambda đến khi chúng ta chỉ ánh xạ hàm add lên một số duy nhất, tức là truyền thiếu tham số, điều này không thực hiện được trong một số ngôn ngữ như C nhưng biểu thức lambda mới lại trả về cho ta một hàm mới dựa vào phép $\beta$-reduction.

$(\lambda x.\lambda y. x+y) 1 = \lambda y.1 + y\;[y]= \lambda x. 1 + x\;[x]$

Tức là thay vì nhận về error, ta nhận về một hàm mới tương đương với hàm increment. Khi tiếp tục ánh xạ, ta sẽ nhận được kết quả như thông thường.

$(\lambda x. 1 + x)\;4 = 1 + 4 = 5$

1.4. Hàm logic

Giải tích lambda có thể giải thích cho chúng ta cách mà máy tính định nghĩa các kiểu dữ liệu nguyên thủy và các hàm logic nguyên thủy.

Bắt đầu với thứ dễ nhất là kiểu dữ liệu Boolean bao gồm hai giá trị True (T) và False (F). Chúng ta đều đã biết rằng True có nghĩa là đúng và nó tương đương với giá trị 1 và ngược lại với với False. Tuy nhiên bởi vì True được định nghĩa trước, tức là không tồn tại 1 để so sánh với True, nếu có một cách làm hết sức thuần túy, đó là:

$\text{T}: \lambda x. \lambda y. x$ $\text{F}: \lambda x. \lambda y. y$

Thức là True thực chất là một hàm, nhận vào hai tham số và trả về tham số đầu tiên. Khác hẳn với cách suy nghĩ thông thường của chúng ta, tuy nhiên khi nhìn vào biểu thức lambda, các bạn có thể thấy rằng cách định nghĩa này hết sức cơ bản (tức là không có cách định nghĩa nào ngắn gọn hơn).

Điều này dẫn đến cách định nghĩa về các hàm logic cũng hết sức cơ bản như sau, đầu tiên là hàm NOT:

$\text{NOT}: \lambda b.\;b\;F\;T$

Thoạt đầu ý tưởng này có vẻ phức tạp, nhưng nó lại khá ảo diệu khi chúng ta ánh xạ lên giá trị cụ thể (lưu ý rằng T cũng là một biểu thức lambda nên có thể được hàm NOT ánh xạ):

$\text{NOT}\;\text{T}=(\lambda b.\;b\;\text{F}\;\text{T})\;\text{T}$ $=\text{T}\;\text{F}\;\text{T} [b:=\text{T}]$ $=(\lambda x. \lambda y. x)\;\text{F}\;\text{T}=\text{F}$

Tương tự khi ánh xạ NOT lên F:

$\text{NOT}\;\text{F}=(\lambda b.\;b\;\text{F}\;\text{T})\;\text{F}$ $=\text{F}\;\text{F}\;\text{T} [b:=\text{F}]$ $=(\lambda x. \lambda y. y)\;\text{F}\;\text{T}=\text{T}$

Đối với hàm logic phức tạp hơn (nhận vào 2 tham số) như hàm AND chẳng hạn, chúng ta có thể tìm ra cách định nghĩa gần như tương tự:

$\text{AND}: \lambda x. \lambda y.\;x\;y\;\text{F}$

$\text{AND}\;\text{T}\;\text{T} = (\lambda x.\lambda y.\;x\;y\;\text{F})\;\text{T}\;\text{T}$

$=\text{T}\;\text{T}\;\text{F}$

$=(\lambda x. \lambda y. x)\;\text{T}\;\text{F}=\text{T}$

2.3. Biểu thức If

If cũng có thể được mã hóa hết sức cơ bản dưới dạng biểu thức lambda như sau:

$\text{if}= \lambda p.\lambda a. \lambda b.p\;a\;b$

$\text{if}\;\text{T}\;a\;b=(\lambda x.\lambda y. x)\;a\;b=a$

$\text{if}\;\text{F}\;a\;b=(\lambda x.\lambda y. y)\;a\;b=b$

Kết thúc bài 1