幫助中心 | 我的帳號 | 關於我們
進階搜尋
car

同類熱銷排行榜

最近瀏覽的商品

現代類型論的發展與應用

  • 作者：(英)羅朝暉|責編:袁勤勇//楊楓
  • 出版社：清華大學
  • ISBN：9787302660354
  • 出版日期：2024/04/01
  • 裝幀：平裝
  • 頁數：213
人民幣：RMB 68 元      售價：元
放入購物車
加入收藏夾
內容大鋼
    本書是關於現代類型論的專著。與集合論類似，現代類型論是數學及諸多領域的基礎語言。本書介紹了現代類型論（及其元理論），並以自然語言語義學和電腦輔助推理為例對以現代類型論為基礎的應用領域進行深入淺出的討論。作為基礎語言，現代類型論一方面提供了豐富的描述機制，另一方面便於理解與實現，因此與集合論相比有著多方面的優勢。這些優點在實際運用中展示出來：作為範例，書中深入研究了基於現代類型論的自然語言語義學，以加深讀者對此的理解。書中還介紹了以現代類型論為基礎的互動式證明技術在數學形式化、電腦程序驗證及自然語言推理諸方面的應用，進一步展示了使用現代類型論作為基礎語言的優勢。
    本書適合研究自然語言語義學、電腦科學和邏輯學等領域的學者及研究生和對相關內容感興趣的讀者。
作者介紹
(英)羅朝暉|責編:袁勤勇//楊楓
    羅朝暉，現為倫敦大學皇家霍洛威學院電腦系教授，曾就讀於國防科技大學，于1990年在英國愛丁堡大學獲博士學位，之後在愛丁堡大學、杜倫大學和倫敦大學就職，畢其一生精力研究現代類型論及其應用，是該領域的學術帶頭人之一，取得了卓越的研究成果，原創作品包括研究統一類型論的《計算與推理》（1994年由牛津大學出版社出版）和研究自然語言語義學的《基於現代類型論的形式語義學》（2020年由Wiley出版社出版）。本書是作者將多年的研究成果精選后寫成的中文專著，它的出版將有效地推動國內邏輯學、電腦科學、自然語言語義學及有關交叉領域的進一步發展。
目錄
第1章  現代類型論及其應用
  1.1  簡單類型論與現代類型論發展概述
  1.2  現代類型論概論及特點綜述
    1.2.1  基本概念概述
    1.2.2  現代類型論的特點及其與其他形式系統的區別
  1.3  現代類型論的若干應用和本書概述
第2章  現代類型論
  2.1  判斷、上下文及定義性等式
  2.2  類型構造運算元
    2.2.1  函數的依賴類型（Π類型）
    2.2.2  序對的依賴類型（?類型）
    2.2.3  不相交並類型
    2.2.4  有窮類型
  2.3  歸納、遞歸及計算理論
    2.3.1  自然數類型
    2.3.2  列表類型和向量類型
  2.4  類型空間
    2.4.1  Prop：邏輯命題的非直謂類型空間
    2.4.2  直謂類型空間及其描述方式
    2.4.3  類型空間應用舉例
  2.5  子類型理論
    2.5.1  包含性子類型理論及其問題
    2.5.2  強制性子類型理論
    2.5.3  子類型類型空間、類型的（不）相交性和依賴性記錄類型
  2.6  後記
第3章  基於現代類型論的自然語言語義學
  3.1  形式語義學的基礎語言
  3.2  蒙太古語義學
  3.3  MTT語義學：概述及特徵
    3.3.1  MTT語義學發展簡史
    3.3.2  MTT語義學簡例
    3.3.3  豐富的類型結構：通名的類型語義、選擇限制及其他
    3.3.4  子類型理論在MTT語義學中的應用
  3.4  形容詞修飾語義的研究
    3.4.1  相交形容詞
    3.4.2  下屬形容詞
    3.4.3  否定性形容詞
    3.4.4  非承諾形容詞
    3.4.5  關於時態形容詞的討論
  3.5  證明無關性及關於回指語義的說明
    3.5.1  證明無關性及其在MTT語義學中的重要性
    3.5.2  關於驢句及回指語義的討論
  3.6  後記
第4章  現代類型論的擴充及語義學研究
  4.1  標記：類型論的語境描述機制
    4.1.1  標記：常量的描述機制
    4.1.2  標記的引入及語境的描述
    4.1.3  標記中的子類型條目及定義性條目
  4.2  同謂現象及其點類型語義
    4.2.1  同謂現象

    4.2.2  點類型的形式化及同謂現象的MTT語義
    4.2.3  通名的集胚語義：以涉及同謂及量詞的複雜語境為例
  4.3  判斷語義的命題形式
    4.3.1  判斷語義及其命題形式
    4.3.2  異類等式及判斷語義之命題形式的形式化
    4.3.3  避免生成過剩
  4.4  依賴類型在事件語義學中的應用
    4.4.1  事件語義學、它的優勢及有關問題
    4.4.2  依賴事件類型（Ⅰ）：簡單類型論的擴充
    4.4.3  依賴事件類型（Ⅱ）：MTT事件語義學
  4.5  依賴性範疇語法
    4.5.1  依賴性子結構類型論
    4.5.2  語法分析的例子
  4.6  後記
第5章  基於現代類型論的互動式推理
  5.1  現代類型論與互動式證明系統
  5.2  程序規範與驗證
    5.2.1  命令式程序及其規範的形式化及驗證
    5.2.2  類型論中函數式程序的規範及驗證
    5.2.3  程序的模塊化開發及驗證
  5.3  自然語言語義的形式化及推理
    5.3.1  在Coq中實現MTT語義學
    5.3.2  形容詞修飾語義
    5.3.3  Most和驢句的語義
    5.3.4  MTT事件語義學
  5.4  後記
第6章  現代類型論的元理論
  6.1  元理論諸重要性質概述
    6.1.1  與上下文有關的元理論性質
    6.1.2  有關計算的重要性質
  6.2  邏輯框架與歸納模式
    6.2.1  邏輯框架LF
    6.2.2  用LF定義類型論
    6.2.3  歸納模式
  6.3  現代類型論的形式化描述及元理論研究
    6.3.1  統一類型論（UTT）
    6.3.2  強制性子類型理論
    6.3.3  標記類型論
  6.4  關於意義理論的討論
  6.5  後記
結語
附錄A  有關上下文和定義性等式的推理規則
附錄B  類型構造運算元的推理規則
  B.1  Π類型
  B.2  ?類型
  B.3  不相交並類型
  B.4  有窮類型
  B.5  自然數類型、列表類型和向量類型
附錄C  Prop及邏輯運算元
  C.1  Prop

  C.2  邏輯算符
附錄D  簡單類型論C
  D.1  C的推理規則
  D.2  C中的邏輯運算符
附錄E  依賴性子結構類型論λΠ
參考文獻
索引

  • 商品搜索：
  • | 高級搜索
首頁│ 新手上路│ 客服中心│ 關於我們│ 聯絡我們│ Top↑│
Copyrightc 1999~2008 美商天龍國際圖書股份有限公司 臺灣分公司. All rights reserved.
營業地址:臺北市中正區重慶南路一段103號1F 105號1F-2F
讀者服務部電話：02-2381-2033 02-2381-1863　時間：週一-週五 10:00-17:00
　服務信箱：bookuu@69book.com 客戶、意見信箱:cs@69book.com
ICP證：浙B2-20060032