是指軟體工程中的典型程式設計風格之一。不同的程式語言會提倡不同的程式設計方式，而不同的程式設計風格也會有各自的優缺點。Functional programming 的價值觀為將所有的計算都視為數學函式的求值。有參照透明及方便平行計算等特徵。

Lambda calculus 由數學家阿隆佐·邱奇（Alonzo Church）在20世紀30年代首次發表的形式系統。是可比擬最根本程式語言的計算模型。概念上可表達為“清晰地定義什麼是一個可計算函式，而任何可計算函式都可以這種形式表達和求值”。能夠類比圖靈機的計算過程。強調規則運算而非具體的機器。是停機問題證明的先驅。

停機問題問的是“任意程式是否能在有限的時間內結束執行”。是最早的判定性問題。與此相關的圖靈於1936年通過圖靈機的概念，證明了停機問題的不可判定性。與此相關的其他觀念包含理髮師悖論等自我指涉問題。我們課程中，會提供大家判定方法，從根本解決這種自我參照的難題。