Simple Type Theory: A Practical Logic for Expressing and Reasoning about Mathematical Ideas
暫譯: 簡單類型理論：表達和推理數學思想的實用邏輯

Farmer, William M.

Simple Type Theory: A Practical Logic for Expressing and Reasoning about Mathematical Ideas
  • 出版商: Birkhauser Boston
  • 出版日期: 2025-04-24
  • 售價: $3,500
  • 貴賓價: 9.5 折 $3,325
  • 語言: 英文
  • 頁數: 319
  • 裝訂: Hardcover - also called cloth, retail trade, or trade
  • ISBN: 3031853512
  • ISBN-13: 9783031853517

    • 海外代購書籍(需單獨結帳)

相關主題

商品描述

This unique textbook, in contrast to a standard logic text, provides the reader with a logic that can be used in practice to express and reason about mathematical ideas. The book is an introduction to simple type theory, a classical higher-order version of predicate logic that extends first-order logic.

It presents a practice-oriented logic called Alonzo that is based on Alonzo Church's formulation of simple type theory known as Church's type theory. Unlike traditional predicate logics, Alonzo admits undefined expressions. The book illustrates using Alonzo how simple type theory is suited ideally for reasoning about mathematical structures and constructing libraries of mathematical knowledge. For this second edition, more than 400 additions, corrections, and improvements have been made, including a new chapter on inductive sets and types.

Topics and features:

- - - - - -

Aimed at students of mathematics and computing at the graduate or upper-undergraduate level, this book is well suited for mathematicians, computing professionals, engineers, and scientists who need a practical logic for expressing and reasoning about mathematical ideas.

William M. Farmer is a Professor in the Department of Computing and Software at McMaster University in Hamilton, Ontario, Canada.

商品描述(中文翻譯)

這本獨特的教科書與標準邏輯教材不同，提供讀者一種可以在實踐中使用的邏輯，以表達和推理數學概念。本書是對於簡單類型理論（simple type theory）的介紹，這是一種經典的高階謂詞邏輯版本，擴展了第一階邏輯。

本書介紹了一種以阿隆佐·丘奇（Alonzo Church）所提出的簡單類型理論（Church's type theory）為基礎的實踐導向邏輯，稱為阿隆佐（Alonzo）。與傳統的謂詞邏輯不同，阿隆佐允許未定義的表達式。本書展示了如何使用阿隆佐，簡單類型理論非常適合用於推理數學結構和構建數學知識庫。對於這個第二版，已進行了超過400項的新增、修正和改進，包括一章關於歸納集合和類型的新章節。

主題和特點：

本書針對研究生或高年級本科生的數學和計算機科學學生，特別適合需要一種實用邏輯來表達和推理數學概念的數學家、計算專業人士、工程師和科學家。

威廉·M·法默（William M. Farmer）是加拿大安大略省漢密爾頓的麥克馬斯特大學計算與軟體系所的教授。

作者簡介

William M. Farmer has 40 years of experience working in industry and
academia in computing and mathematics. He received a B.A. in
mathematics from the University of Notre Dame in 1978 and an M.A. in
mathematics in 1980, an M.S. in computer sciences in 1983, and a
Ph.D. in mathematics in 1984 from the University of Wisconsin-Madison.
He is currently a Professor in the Department of Computing and
Software at McMaster University. Before joining McMaster in 1999, he
conducted research in computer science for twelve years at The MITRE
Corporation in Bedford, Massachusetts, USA and taught computer
programming and networking courses for two years at St. Cloud State
University.

Dr. Farmer's research interests are logic, mathematical knowledge
management, mechanized mathematics, and formal methods. One of his
most significant achievements is the design and implementation of the
IMPS proof assistant, which was done at MITRE in partnership with
Dr. Joshua Guttman and Dr. Javier Thayer. His work on IMPS has led to
research on developing practical logics based on simple type theory
and NGB set theory and on organizing mathematical knowledge as a
network of interconnected axiomatic theories. He also has
collaborated with Dr. Jacques Carette for several years at McMaster on
developing a framework for integrating axiomatic and algorithmic
mathematics. As part of this research, Dr. Farmer has investigated
how to reason about the interplay of syntax and semantics, as
exhibited in syntax-based mathematical algorithms like symbolic
differentiation, within a logic equipped with global quotation and
evaluation operators. Dr. Farmer is currently working on developing a
communication-oriented approach to formal mathematics as an
alternative to the standard certification-oriented approach employed
using proof assistants.

作者簡介(中文翻譯)

威廉·M·法默（William M. Farmer）在計算和數學領域擁有40年的產業和學術經驗。他於1978年獲得聖母大學（University of Notre Dame）的數學學士學位，1980年獲得數學碩士學位，1983年獲得計算機科學碩士學位，並於1984年獲得威斯康辛大學麥迪遜分校（University of Wisconsin-Madison）的數學博士學位。他目前是麥克馬斯特大學（McMaster University）計算與軟體系所的教授。在1999年加入麥克馬斯特大學之前，他在美國麻薩諸塞州貝德福德的MITRE公司從事了十二年的計算機科學研究，並在聖克勞德州立大學（St. Cloud State University）教授了兩年的計算機程式設計和網路課程。

法默博士的研究興趣包括邏輯、數學知識管理、機械化數學和形式方法。他最重要的成就之一是設計和實現IMPS證明助手，這項工作是在MITRE與喬舒亞·古特曼博士（Dr. Joshua Guttman）和哈維爾·泰爾博士（Dr. Javier Thayer）合作完成的。他在IMPS上的工作促進了基於簡單類型理論和NGB集合論的實用邏輯的研究，以及將數學知識組織為相互連結的公理理論網絡。他還與麥克馬斯特大學的雅克·卡雷特博士（Dr. Jacques Carette）合作多年，開發一個整合公理數學和算法數學的框架。在這項研究中，法默博士探討了如何在具備全域引用和評估運算子的邏輯中，推理語法和語義之間的相互作用，這在基於語法的數學算法（如符號微分）中得以體現。法默博士目前正在開發一種以溝通為導向的形式數學方法，作為使用證明助手的標準認證導向方法的替代方案。

類似商品