《科學計算導論》與另一本書名十分相似的書📚《計算科學導論》，分別是兩本完全不同的教材，大家千萬不要搞混淆，買錯教材了。 [偷笑] 前者更接近於應用數學或是信息科學裡的數值分析，而後者則大致等同於計算機導論——前者是專業基礎課，而後者則更相當於是准公共課程。 —— —— Homotopy Type Theory. （HoTT）是指一種將「代數拓撲同倫論」與「類型論」相融合的數學基礎理論，其核心概念建立於類型論與同倫論的交叉之上，它在數學與計算機科學領域均有著深遠的影響。它通過引入「高階歸納類型和合成同倫論」等概念，試圖在「數學形式化和計算機科學」之間建立起一種新的聯繫。具體來講，「同倫類型論」是一種基於「馬丁·洛夫構造類型論」（又名「直覺類型論」或「依賴類型論」，1972 瑞典數學哲學家提出的基於「數學構造主義」的邏輯框架，它同時融合了函數式編程語言，邏輯學與集合論）的擴展，它允許類型內部的元素通過同倫路徑來進行連接，從而「將類型視作高維範疇結構」。——該理論不僅為數學對象的「構造性和抽象同倫論」提供了一種統一的語言，還在「人工智能輔助證明」和「形式化數學」中展現出巨大的潛力和威力。它的核心創新思想有三： 「Univalence 公理」（等價即同一）；高階歸納類型（HITs）；命題等於＝「可收縮類型」。此外，同倫類型論通過引入「單價公理」，使得「類型等價與對象同倫等價」可以直接對應，從而為數學基礎和形式化提供了新的視角（認識論）與方法論！——HoTT 是聯結（或鏈接🔗）純粹數學與理論計算機科學之間的橋樑，既為數學提供了結構優先的基礎框架，也同為編程語言之設計與形式化驗證開闢了嶄新方向！ #代數拓撲同倫論與類型論# #構造類型論的三大理論基石# #數學形式化和理論計算機科學# #數學構造主義# #集合論和同倫類型論#