Alonzo Church: kiến trúc sư bị lãng quên của trí tuệ máy tính

• Alonzo Church không nổi tiếng rộng rãi như Alan Turing, nhưng là một nhà logic học đã đặt nền móng logic cho điện toán bằng λ-calculus và lý thuyết tính khả tính
• Năm 1936, luận đề Church-Turing đã đưa ra khuôn khổ rằng các hàm có thể tính được một cách hiệu quả đều có thể được tính bởi máy Turing hoặc một hệ tương đương
• Khi trả lời Entscheidungsproblem của Hilbert, ông cho thấy không tồn tại thuật toán quyết định nào có thể phán định mọi mệnh đề toán học, qua đó làm rõ các giới hạn của tính toán
• Tại Princeton, ông hướng dẫn Stephen Kleene, J. Barkley Rosser, Alan Turing và những người khác; Turing hoàn thành bằng Ph.D. dưới sự hướng dẫn của Church
• Công trình trừu tượng của ông vẫn hiện diện trong phả hệ của tính toán hiện đại, từ compiler, interpreter, lập trình hàm cho tới ứng dụng smartphone và AI

---

Ảnh hưởng lý thuyết lớn hơn danh tiếng đại chúng

• Alan Turing thường được nhắc đến nhiều hơn trong lịch sử đại chúng của điện toán và trí tuệ nhân tạo nhờ Turing Test, nhưng Church là người có ảnh hưởng lớn đến tư duy và công trình của Turing
• Công trình của Church là nền tảng quan trọng để hình thành các khái niệm về việc tính toán là gì và cách đánh giá AI
• Nếu không có những đóng góp của Church, các khái niệm hiện nay về trí tuệ nhân tạo và cách đánh giá nó có thể đã rất khác

Cuộc đời và khuynh hướng học thuật

• Church là một nhà logic học trầm lặng, ít nói, sinh ngày 14 tháng 6 năm 1903 tại Washington, D.C.
• Có ghi chép cho rằng thời thơ ấu ông bị mù một mắt hoặc mất một phần thị lực sau một tai nạn súng hơi
• Sau khi hoàn thành trường dự bị tại Connecticut vào năm 1920, ông bắt đầu học đại học ở Princeton ngay trong năm đó và hoàn tất bậc tiến sĩ vào năm 1927
• Sau thời gian làm National Research Fellow tại Harvard, Göttingen và Amsterdam, ông trở lại Princeton và xây dựng phần lớn thành tựu học thuật của mình tại đó
• Ông được biết đến với chữ viết bảng rất gọn gàng và tính cách tỉ mỉ, thậm chí từng phủ Duco cement lên các bài báo quan trọng để bảo quản chúng

λ-calculus và tính khả tính

• Đóng góp sâu sắc nhất của Church là λ-calculus, nền tảng được đặt ra trước cả khi cái tên khoa học máy tính xuất hiện
• Năm 1936, Church đã chính thức hóa luận đề Church-Turing, một khái niệm cốt lõi của khoa học máy tính lý thuyết
  • Nội dung của nó là các hàm có thể tính được một cách hiệu quả đều có thể được tính bởi máy Turing hoặc một hệ tương đương
  • Nó cung cấp khuôn khổ để hiểu về mặt lý thuyết máy móc có thể làm được gì
  • Đồng thời nó cũng chỉ ra ranh giới mà các thủ tục thuật toán có thể chạm tới
• Đây là một khái niệm nền tảng, nhưng vẫn để lại các tranh luận và giới hạn xoay quanh cách diễn giải ‘effective computability’, tính toán vật lý và bản chất của trí tuệ con người
• Nếu Turing đề xuất máy Turing để chuyển các thủ tục cơ học sang dạng logic, thì Church đã cung cấp sự trừu tượng thuần túy làm nền tảng lý thuyết cho những cỗ máy đó

Lập trình hiện đại và tư duy hàm

• Ảnh hưởng của λ-calculus còn thể hiện trong các nguyên lý viết chương trình ngày nay, gắn với cách tiếp cận nhấn mạnh composition, hàm bậc cao và tính bất biến
• Hệ hình thức này cho phép mã hóa các bài toán toán học trừu tượng và giải chúng một cách cơ học, đồng thời trở thành nền tảng cho kiến trúc compiler và interpreter hiện đại
• Với lập trình viên ngày nay, λ-calculus có thể trông như một tập hợp các hàm lồng nhau, tương tự những paradigm có thể thấy trong Lisp, Haskell, hoặc một phần của Python và JavaScript
• Sự trừu tượng của λ-calculus là nền tảng của lập trình hàm, nơi các hàm được đối xử như first-class citizen

Entscheidungsproblem và giới hạn của tính toán

• Church cũng có những đóng góp quan trọng cho các lĩnh vực khác của logic và triết học, trong đó ví dụ tiêu biểu là công trình về Entscheidungsproblem
• Entscheidungsproblem là bài toán quyết định do David Hilbert nêu ra vào năm 1928, đặt câu hỏi liệu có tồn tại một thuật toán quyết định có thể xác định tính đúng sai của mọi mệnh đề toán học hay không
• Church đã đưa ra câu trả lời phủ định rằng thuật toán như vậy không tồn tại, và kết quả này được biết đến với tên Định lý Church
• Phát hiện này có ảnh hưởng sâu sắc đến lý thuyết quyết định và nhấn mạnh giới hạn của những gì có thể đạt được chỉ bằng tính toán

Trung tâm trí tuệ của Princeton và các học trò

• Church là một người thầy đã hướng dẫn nhiều nhà logic học và nhà khoa học máy tính quan trọng của thời đại
• Phả hệ học thuật của ông bao gồm Stephen Kleene, J. Barkley Rosser và Alan Turing
• Turing hoàn thành bằng Ph.D. tại Princeton dưới sự hướng dẫn của Church
• Tương truyền David Kaplan từng khuyên các nghiên cứu sinh mới hãy thử học lớp của Church, nói rằng ngay cả khi đó không phải lĩnh vực quan tâm của họ thì đây vẫn sẽ là trải nghiệm để kể lại cho cháu chắt sau này
• Princeton những năm 1930 là trung tâm trí tuệ của sự phát triển logic hiện đại, nơi có John von Neumann, Kurt Gödel và Church cùng hiện diện

Di sản ít được nhìn thấy

• So với Turing, von Neumann hay Gödel, Church không đạt được mức độ danh tiếng đại chúng tương đương
• Di sản của ông không mang dáng dấp dễ khơi gợi trí tưởng tượng đại chúng như những câu chuyện anh hùng giải mã thời chiến hay bi kịch ra đi sớm
• Hàng tỷ chương trình chạy trên smartphone ngày nay có thể lần theo logic của chúng ngược về các hàm trừu tượng của λ-calculus
• Từ các ứng dụng đơn giản đến trí tuệ nhân tạo, DNA vô hình của tính toán tiếp nối một phả hệ quan trọng từ công trình của Church
• Thiên tài của Church không nằm ở sự ngoạn mục, mà ở cấu trúc chặt chẽ và vẻ thanh nhã thầm lặng đã làm thay đổi thế giới

[GN⁺]

Các ý kiến trên Hacker News

• Tôi thích phần nguồn gốc của tên lambda trong Paradigms of Artificial Intelligence Programming (PDF/EPUB: https://github.com/norvig/paip-lisp)
  Câu chuyện là Alonzo Church muốn biến ký hiệu dấu mũ đặt trên biến bị ràng buộc trong ký pháp Principia Mathematica của Russell và Whitehead, x̂(x + x), thành chuỗi một chiều nên đã chuyển nó ra phía trước như ^x(x + x); vì dấu mũ trống trông kỳ nên đổi thành lambda viết hoa Λx(x + x), rồi để tránh nhầm lẫn thì thành chữ thường λx(x + x)
  Nội dung cũng nói rằng John McCarthy từng là sinh viên của Church ở Princeton, và khi tạo Lisp năm 1958, do máy keypunch thời đó không có chữ Hy Lạp nên ông dùng (lambda (x) (+ x x)), và cách viết ấy còn tồn tại đến nay
  Vì vậy, đúng như chủ đề của bài này, Church thường xuyên xuất hiện trong các hồi tưởng về Lisp; ông chỉ có thể là nhân vật “bị lãng quên” đối với những người hầu như không quan tâm đến lịch sử điện toán

  • Tôi đã hy vọng nguồn gốc đó có ý nghĩa hơn một ký hiệu khó hiểu, nhưng thực tế có vẻ không phải vậy
    Theo Dana Scott, bản thân Church nói lựa chọn đó là một lựa chọn tùy ý kiểu “eeny, meeny, miny, moe”, và cách giải thích kiểu Barendregt cũng được cho là đã bị phản bác trong một bài giảng gần đây tại University of Birmingham
    Trong khối Pháp ngữ, “personne lambda” có nghĩa là người bình thường/người vô danh, nên trông khá hợp với hàm ẩn danh; tính từ lambda cũng có nghĩa là “chung/chẳng có gì đặc biệt”, nên có cảm giác một chữ cái ở khoảng giữa bảng chữ cái Hy Lạp biểu thị cái gì đó trung bình
    https://math.stackexchange.com/questions/64468/why-is-lambda...
  • Tuy nói “Lisp thường chuộng những cái tên có tính biểu đạt”, nhưng ngoài lambda ra, car/cdr dù không phải chữ Hy Lạp cũng hoàn toàn không phải tên trong suốt
  • PAIP là một cuốn sách xuất sắc xét tổng thể, dù bản thân chủ đề trí tuệ nhân tạo đã khá có tuổi
    Sách đề cập nhiều chủ đề lập trình và cũng mở ra những paradigm có thể xa lạ với người ít tiếp xúc với lập trình hàm
  • Không rõ câu chuyện lặp đi lặp lại này về nguồn gốc ký pháp lambda của Alonzo Church có đúng hay không
    Một trường hợp khác ám chỉ rằng Church chọn gần như tùy ý trong số các chữ cái Hy Lạp, hơn là vì một ý nghĩa cụ thể, có ở https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...
  • Tôi tò mò ai là người đầu tiên đặt ra thuật ngữ lambda calculus
    Cũng tò mò việc đó xảy ra trước hay sau khi McCarthy bắt đầu Lisp

• “Phép tính lambda của Church và máy Turing có năng lực tính toán tương đương, nhưng khác ở chỗ máy Turing dùng trạng thái khả biến. Việc đến tận ngày nay vẫn có một rạn nứt giữa ngôn ngữ hàm và ngôn ngữ mệnh lệnh là do sự tách biệt giữa Church và state”
  Tôi đã biết câu trích này từ lâu nhưng không tìm được nguồn gốc
  Chỉnh sửa: Có thể nó đến từ câu của Guy Steele: “Có những người không muốn trộn phần hàm/lambda calculus của ngôn ngữ với phần gây ra tác dụng phụ. Có vẻ họ tin vào sự tách biệt giữa Church và state”

  • Câu trích đó của Guy xuất phát từ danh sách thư của MIT tiếp sau Lightweight Languages Workshop 2001
    Bản lưu trữ gốc ở đây: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
  • Tôi cũng nhớ đến trò đùa về tên Niklaus Wirth
    Người châu Âu nhìn chung phát âm đúng tên ông là “Nick-louse Veert”, nhưng người Mỹ thì làm hỏng thành “Nickel's Worth”
    Tức là người châu Âu gọi ông bằng tên, còn người Mỹ gọi ông bằng giá trị
    https://en.m.wikiquote.org/wiki/Niklaus_Wirth
  • Có vẻ là từ phía Peter Norvig. Xem bình luận anh em là thấy

• Nếu muốn đọc một bài thật sự đáng kinh ngạc về Church, tôi khuyên đọc hồi ký của Rota
  Đó là mục đầu tiên tại https://www34.homepage.villanova.edu/robert.jantzen/princeto...
  Các liên kết liên quan gồm Alonzo Church, 92, Theorist of the Limits of Mathematics (1995) - https://news.ycombinator.com/item?id=12240815 - tháng 8/2016, và Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - tháng 2/2015

  • Hồi ký của Rota không chỉ có phần về Church; toàn bộ trang web, tức “Fine Hall in its golden age: Remembrances of Princeton in the early fifties”, là một chương trong cuốn Indiscrete Thoughts của ông
    Cả cuốn sách đều đáng đọc

• Ngôn ngữ lập trình Alonzo mang tên ông thì gần như đã bị lãng quên
  https://dl.acm.org/doi/pdf/10.1145/68127.68139

• Đặc biệt, triết học logic nối tiếp công trình của Frege và Russell, cùng các lý thuyết về nghĩa/quy chiếu, phần lớn đã bị lãng quên
  Church đã công bố nhiều bài về chủ đề này, nhưng những nơi như Wikipedia hầu như không đề cập
  Dù vậy, mục trong Stanford Encyclopedia of Philosophy thì khá hơn một chút: https://plato.stanford.edu/entries/church/
  Tuy nhiên, tôi nghe nói ngay cả mục đó cũng bỏ sót một phần các công trình chính của ông, và có lẽ nó quá triết học đối với các nhà toán học, nhưng lại quá kỹ thuật đối với các triết gia

  • Liên quan đến điều này, E.J. Lemmon, khi điểm ra những cuốn sách logic quan trọng trong Beginning Logic, đã viết rằng chương 0 của Introduction to Mathematical Logic của Church đáng để mọi triết gia đọc đi đọc lại nhiều lần

• Không phải luận điểm cốt lõi, nhưng tôi mong các bài blog nên hạn chế dùng minh họa do AI tạo
  Ảnh thật của Church cũng có trong phạm vi công cộng, còn minh họa này không thực sự giống ông, và khi bài viết trở nên phổ biến, nó đã xuất hiện trong kết quả tìm kiếm hình ảnh
  Nếu đó là một minh họa đến mức không đáng dành hơn 5 phút để tạo, thì có lẽ bỏ hẳn đi sẽ tốt hơn
  Dù vậy, nếu nhất thiết phải dùng ảnh do “AI” tạo, tối thiểu cũng nên chú thích như vậy

  • Cảm ơn đã chỉ ra và xin lỗi
    Tôi không thấy thoải mái khi lấy ảnh trên mạng, và hình này là kết quả thứ 7 tôi tạo ra để nó không trở thành một chân dung giống ‘giả’, và tôi cảm thấy nó cũng giống ở mức nào đó
    Ảnh JvN thì tạo khá tốt, nhưng về sau có lẽ dùng hình ảnh mang tính biểu tượng thay cho chân dung giả trông như người thật sẽ đúng hơn

• Cụm “kiến trúc sư của trí tuệ máy tính” có vẻ hơi quá
  Đúng là Church là một nhà logic học xuất sắc, nhưng nếu trí tuệ máy tính ở đây nghĩa là AI/ML thì đóng góp của ông gần như không có
  Riêng chuyện phép tính lambda có thực sự là toán học hay không thì tôi cũng không chắc, nó trông giống một hệ ký hiệu thông minh hơn
  Ưu điểm của ký hiệu là chuyện chủ quan, và việc Church không mấy quan tâm đến chuyện ý tưởng của mình đã truyền cảm hứng cho thiết kế một số ngôn ngữ lập trình cụ thể cũng khá thú vị

  • “Lambda calculus” đôi khi có nghĩa là phép tính lambda có kiểu đơn giản, thường được dùng để chỉ lý thuyết kiểu đơn giản (STT), tức “lý thuyết kiểu của Church”
    STT cũng thường được đồng nhất với logic bậc cao, vì chỉ với hai kiểu nguyên thủy là “đối tượng” cơ bản và giá trị chân lý T/F, cùng kiểu hàm (a --> b), nó có thể biểu diễn mọi đối tượng logic tùy ý
    STT rõ ràng là phát minh của Church, đã ảnh hưởng lớn đến các lý thuyết kiểu hiện đại, và cũng ảnh hưởng đến các ngôn ngữ lập trình có hệ thống kiểu phức tạp như Haskell

• Không thể chứng minh hoàn toàn, nhưng theo trực giác của tôi, Turing và những gì ông đại diện rốt cuộc được đánh giá cao trong AI, còn Church thì có vẻ ngược lại
  Người trước xuất phát từ sự thuần khiết, các điều kiện tối thiểu có thể, và tính toán trừu tượng, “thuần túy”; còn người sau quan tâm đến việc chúng ta thực sự có thể suy nghĩ như thế nào, và dường như chú trọng hơn đến việc mở rộng biểu đạt và trừu tượng hóa hơn là triển khai

  • Nhìn từ một góc độ, Turing đã tạo ra máy tính thực dụng trong thời chiến, nhưng sau đó bị chính phủ của mình ngăn không cho tiếp tục chế tạo máy tính, nên phải lùi về lý thuyết
    Church không có kinh nghiệm thực hành với máy tính và gần với hướng mở rộng chính lý thuyết toán học hơn
    Sự cộng tác và trao đổi xuyên Đại Tây Dương giữa hai người đã kết hợp thực tiễn với lý thuyết, làm vững chắc các lý thuyết cốt lõi như lưỡng tính mệnh lệnh/hàm, định lý Church-Turing, quan hệ giữa bài toán dừng và định lý Church
    Xem họ như đối thủ cạnh tranh là sai, và nói rằng khoa học máy tính có “hai người cha” là phù hợp vì nhiều lý do
    Đặc biệt là khi nghĩ đến cái chết của Turing
    Ngoài ra, Turing không phải là không quan tâm đến triển khai; không nên bỏ qua việc ông thật sự muốn quay lại triển khai thực tế nhưng không được phép
    Nếu cách chính phủ Anh phân loại bí mật khác đi thì vẫn còn đó một bi kịch và câu hỏi lớn về điều gì đã có thể thay đổi, nhưng nếu vậy có lẽ chúng ta cũng đã mất đi sự cộng tác với Church, người đã giúp củng cố lý thuyết rất tốt trong dòng thời gian của chúng ta

• Tôi đã may mắn được gặp Alonzo Church và Haskell Curry tại ACM Symposium on LISP and Functional Programming tổ chức ở CMU vào tháng 8 năm 1982
  Curry rõ ràng sức khỏe không tốt và qua đời khoảng 2 tuần sau hội nghị, nhưng Church trông khỏe mạnh và sống thêm khoảng 13 năm nữa
  Tại buổi tiếp tân, Gerry Sussman rất hào hứng khi đi quanh phòng và giới thiệu hai người; với chúng tôi, được gặp họ cũng là một niềm xúc động lớn

• Một trong những đóng góp lớn của Church là các học trò của ông
  Một loạt nhà tư tưởng đáng kinh ngạc đã xuất hiện từ cùng một nơi