arXiv subjects

William M. Farmer

Publications and source records attributed to William M. Farmer.

At least 19 recordsLinked to original sources

arXiv2026

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility

Formal mathematics is mathematics done within the framework of a formal logic. It offers major benefits to mathematicians as well as to computing professionals, engineers, and scientists who use mathematics in their work. The standard approach to formal mathematics, in which mathematics is done with the help of a proof assistant and all details are formally proved and mechanically checked, achieves these benefits and offers a very high level of assurance that the results produced are correct. However, since the main goal of the standard approach is certification, the proof assistants supporting the standard approach are generally complex, based on unfamiliar logics, difficult to learn how to use, and far removed from mathematical practice. Thus the standard approach does not adequately serve mathematics practitioners who are more interested in communicating mathematical ideas than in formally certifying their correctness or who prefer not to make the investment needed to gain proficiency in the use of a proof assistant. This paper presents an alternative to the standard approach that focuses on communication and accessibility, the two weaknesses of the standard approach. It is called the free approach to formal mathematics since it is free of the obligation to formally prove and mechanically check all details of a mathematical development. The paper argues that the free approach would serve the needs of the average mathematics practitioner much better than the standard approach. It describes an implementation of the free approach based on a logic named Alonzo, a practice-oriented version of Alonzo Church's formulation of simple type theory. And it calls for the mathematics community to develop logics, software, and libraries of formal mathematical knowledge to support the free approach and to train mathematics practitioners to use them.

math.LO↗

arXiv2025

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory

Alonzo is a practice-oriented classical higher-order version of predicate logic that extends first-order logic and that admits undefined expressions. Named in honor of Alonzo Church, Alonzo is based on Church's type theory, Church's formulation of simple type theory. The little theories method is a method for formalizing mathematical knowledge as a theory graph consisting of theories as nodes and theory morphisms as directed edges. The development of a mathematical topic is done in the "little theory" in the theory graph that has the most convenient level of abstraction and the most convenient vocabulary, and then the definitions and theorems produced in the development are transported, as needed, to other theories via the theory morphisms in the theory graph. The purpose of this paper is to illustrate how a body of mathematical knowledge can be formalized in Alonzo using the little theories method. This is done by formalizing monoid theory -- the body of mathematical knowledge about monoids -- in Alonzo. Instead of using the standard approach to formal mathematics in which mathematics is done with the help of a proof assistant and all details are formally proved and mechanically checked, we employ an alternative approach in which everything is done within a formal logic but proofs are not required to be fully formal. The standard approach focuses on certification, while this alternative approach focuses on communication and accessibility.

cs.LO↗

arXiv2020

Leveraging the Information Contained in Theory Presentations

A theorem prover without an extensive library is much less useful to its potential users. Algebra, the study of algebraic structures, is a core component of such libraries. Algebraic theories also are themselves structured, the study of which was started as Universal Algebra. Various constructions (homomorphism, term algebras, products, etc) and their properties are both universal and constructive. Thus they are ripe for being automated. Unfortunately, current practice still requires library builders to write these by hand. We first highlight specific redundancies in libraries of existing systems. Then we describe a framework for generating these derived concepts from theory definitions. We demonstrate the usefulness of this framework on a test library of 227 theories.

cs.LO↗

arXiv2020

The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems

Mathematical software systems are becoming more and more important in pure and applied mathematics in order to deal with the complexity and scalability issues inherent in mathematics. In the last decades we have seen a cambric explosion of increasingly powerful but also diverging systems. To give researchers a guide to this space of systems, we devise a novel conceptualization of mathematical software that focuses on five aspects: inference covers formal logic and reasoning about mathematical statements via proofs and models, typically with strong emphasis on correctness; computation covers algorithms and software libraries for representing and manipulating mathematical objects, typically with strong emphasis on efficiency; concretization covers generating and maintaining collections of mathematical objects conforming to a certain pattern, typically with strong emphasis on complete enumeration; narration covers describing mathematical contexts and relations, typically with strong emphasis on human readability; finally, organization covers representing mathematical contexts and objects in machine-actionable formal languages, typically with strong emphasis on expressivity and system interoperability. Despite broad agreement that an ideal system would seamlessly integrate all these aspects, research has diversified into families of highly specialized systems focusing on a single aspect and possibly partially integrating others, each with their own communities, challenges, and successes. In this survey, we focus on the commonalities and differences of these systems from the perspective of a future multi-aspect system.

cs.MS↗

arXiv2019

Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal

Over the last decades, a class of important mathematical results have required an ever increasing amount of human effort to carry out. For some, the help of computers is now indispensable. We analyze the implications of this trend towards "big mathematics", its relation to human cognition, and how machine support for big math can be organized. The central contribution of this position paper is an information model for "doing mathematics", which posits that humans very efficiently integrate four aspects: inference, computation, tabulation, and narration around a well-organized core of mathematical knowledge. The challenge for mathematical software systems is that these four aspects need to be integrated as well. We briefly survey the state of the art.

cs.MS↗

arXiv2019

Towards Specifying Symbolic Computation

Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways. Although these algorithms are commonplace in computer algebra systems, they can be surprisingly difficult to specify in a formal logic since they involve an interplay of syntax and semantics. In this paper we discuss several examples of syntax-based mathematical algorithms, and we show how to specify them in a formal logic with undefinedness, quotation, and evaluation.

cs.LO↗

arXiv2018

A New Style of Proof for Mathematics Organized as a Network of Axiomatic Theories

A theory graph is a network of axiomatic theories connected with meaning-preserving mappings called theory morphisms. Theory graphs are well suited for organizing large bodies of mathematical knowledge. Traditional and formal proofs do not adequately fulfill all the purposes that mathematical proofs have, and they do not exploit the structure inherent in a theory graph. We propose a new style of proof that fulfills the principal purposes of a mathematical proof as well as capitalizes on the connections provided by the theory morphisms in a theory graph. This new style of proof combines the strengths of traditional proofs with the strengths of formal proofs.

cs.LO↗

arXiv2018

Biform Theories: Project Description

A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for specifying and reasoning about algorithms that manipulate mathematical expressions. However, formalizing biform theories is challenging since it requires the means to express statements about the interplay of what these algorithms do and what their actions mean mathematically. This paper describes a project to develop a methodology for expressing, manipulating, managing, and generating mathematical knowledge as a network of biform theories. It is a subproject of MathScheme, a long-term project at McMaster University to produce a framework for integrating formal deduction and symbolic computation.

cs.LO↗

arXiv2018

HOL Light QE

We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators, akin to quote and eval in the Lisp programming language. Since the HOL logic is also a version of Church's type theory, we decided to add quotation and evaluation to HOL Light to demonstrate the implementability of ${\rm CTT}_{\rm qe}$ and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called HOL Light QE. Here we document the design of HOL Light QE and the challenges that needed to be overcome. The resulting implementation is freely available.

cs.LO↗

arXiv2018

Incorporating Quotation and Evaluation Into Church's Type Theory

${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators that are similar to quote and eval in the Lisp programming language. With quotation and evaluation it is possible to reason in ${\rm CTT}_{\rm qe}$ about the interplay of the syntax and semantics of expressions and, as a result, to formalize syntax-based mathematical algorithms. We present the syntax and semantics of ${\rm CTT}_{\rm qe}$ as well as a proof system for ${\rm CTT}_{\rm qe}$. The proof system is shown to be sound for all formulas and complete for formulas that do not contain evaluations. We give several examples that illustrate the usefulness of having quotation and evaluation in ${\rm CTT}_{\rm qe}$.

cs.LO↗

arXiv2017

Theory Morphisms in Church's Type Theory with Quotation and Evaluation

${\rm CTT}_{\rm qe}$ is a version of Church's type theory with global quotation and evaluation operators that is engineered to reason about the interplay of syntax and semantics and to formalize syntax-based mathematical algorithms. ${\rm CTT}_{\rm uqe}$ is a variant of ${\rm CTT}_{\rm qe}$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than ${\rm CTT}_{\rm qe}$ as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of ${\rm CTT}_{\rm uqe}$, defines a notion of a theory morphism from one ${\rm CTT}_{\rm uqe}$ theory to another, and gives two simple examples that illustrate the use of theory morphisms in ${\rm CTT}_{\rm uqe}$.

cs.LO↗

arXiv2017

Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study

A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for formalizing algorithms that manipulate mathematical expressions. A theory graph is a network of theories connected by meaning-preserving theory morphisms that map the formulas of one theory to the formulas of another theory. Theory graphs are in turn well suited for formalizing mathematical knowledge at the most convenient level of abstraction using the most convenient vocabulary. We are interested in the problem of whether a body of mathematical knowledge can be effectively formalized as a theory graph of biform theories. As a test case, we look at the graph of theories encoding natural number arithmetic. We used two different formalisms to do this, which we describe and compare. The first is realized in ${\rm CTT}_{\rm uqe}$, a version of Church's type theory with quotation and evaluation, and the second is realized in Agda, a dependently typed programming language.

cs.LO↗

arXiv2016

Simple Type Theory with Undefinedness, Quotation, and Evaluation

This paper presents a version of simple type theory called ${\cal Q}^{\rm uqe}_{0}$ that is based on ${\cal Q}_0$, the elegant formulation of Church's type theory created and extensively studied by Peter B. Andrews. ${\cal Q}^{\rm uqe}_{0}$ directly formalizes the traditional approach to undefinedness in which undefined expressions are treated as legitimate, nondenoting expressions that can be components of meaningful statements. ${\cal Q}^{\rm uqe}_{0}$ is also equipped with a facility for reasoning about the syntax of expressions based on quotation and evaluation. Quotation is used to refer to a syntactic value that represents the syntactic structure of an expression, and evaluation is used to refer to the value of the expression that a syntactic value represents. With quotation and evaluation it is possible to reason in ${\cal Q}^{\rm uqe}_{0}$ about the interplay of the syntax and semantics of expressions and, as a result, to formalize in ${\cal Q}^{\rm uqe}_{0}$ syntax-based mathematical algorithms. The paper gives the syntax and semantics of ${\cal Q}^{\rm uqe}_{0}$ as well as a proof system for ${\cal Q}^{\rm uqe}_{0}$. The proof system is shown to be sound for all formulas and complete for formulas that do not contain evaluations. The paper also illustrates some applications of ${\cal Q}^{\rm uqe}_{0}$.

math.LO↗

arXiv2016

Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics

${\rm \small CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators that are similar to quote and eval in the Lisp programming language. With quotation and evaluation it is possible to reason in ${\rm \small CTT}_{\rm qe}$ about the interplay of the syntax and semantics of expressions and, as a result, to formalize syntax-based mathematical algorithms. We present the syntax and semantics of ${\rm \small CTT}_{\rm qe}$ and give several examples that illustrate the usefulness of having quotation and evaluation in ${\rm \small CTT}_{\rm qe}$. We do not give a proof system for ${\rm \small CTT}_{\rm qe}$, but we do sketch what a proof system could look like.

cs.LO↗

arXiv2014

Andrews' Type Theory with Undefinedness

${\cal Q}_0$ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, ${\cal Q}_0$ does not admit undefined terms. The "traditional approach to undefinedness" in mathematical practice is to treat undefined terms as legitimate, nondenoting terms that can be components of meaningful statements. ${\cal Q}^{\rm u}_{0}$ is a modification of Andrews' type theory ${\cal Q}_0$ that directly formalizes the traditional approach to undefinedness. This paper presents ${\cal Q}^{\rm u}_{0}$ and proves that the proof system of ${\cal Q}^{\rm u}_{0}$ is sound and complete with respect to its semantics which is based on Henkin-style general models. The paper's development of ${\cal Q}^{\rm u}_{0}$ closely follows Andrews' development of ${\cal Q}_0$ to clearly delineate the differences between the two systems.

math.LO↗

arXiv2014

Frameworks for Reasoning about Syntax that Utilize Quotation and Evaluation

It is often useful, if not necessary, to reason about the syntactic structure of an expression in an interpreted language (i.e., a language with a semantics). This paper introduces a mathematical structure called a syntax framework that is intended to be an abstract model of a system for reasoning about the syntax of an interpreted language. Like many concrete systems for reasoning about syntax, a syntax framework contains a mapping of expressions in the interpreted language to syntactic values that represent the syntactic structures of the expressions; a language for reasoning about the syntactic values; a mechanism called quotation to refer to the syntactic value of an expression; and a mechanism called evaluation to refer to the value of the expression represented by a syntactic value. A syntax framework provides a basis for integrating reasoning about the syntax of the expressions with reasoning about what the expressions mean. The notion of a syntax framework is used to discuss how quotation and evaluation can be built into a language and to define what quasiquotation is. Several examples of syntax frameworks are presented.

cs.LO↗

arXiv2014

Realms: A Structure for Consolidating Knowledge about Mathematical Theories

Since there are different ways of axiomatizing and developing a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We introduce the notion of a realm as a structure for consolidating knowledge about a mathematical theory. A realm contains several axiomatizations of a theory that are separately developed. Views interconnect these developments and establish that the axiomatizations are equivalent in the sense of being mutually interpretable. A realm also contains an external interface that is convenient for users of the library who want to apply the concepts and facts of the theory without delving into the details of how the concepts and facts were developed. We illustrate the utility of realms through a series of examples. We also give an outline of the mechanisms that are needed to create and maintain realms.

cs.MS↗

arXiv2013

The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation

Algorithms like those for differentiating functional expressions manipulate the syntactic structure of mathematical expressions in a mathematically meaningful way. A formalization of such an algorithm should include a specification of its computational behavior, a specification of its mathematical meaning, and a mechanism for applying the algorithm to actual expressions. Achieving these goals requires the ability to integrate reasoning about the syntax of the expressions with reasoning about what the expressions mean. A syntax framework is a mathematical structure that is an abstract model for a syntax reasoning system. It contains a mapping of expressions to syntactic values that represent the syntactic structures of the expressions; a language for reasoning about syntactic values; a quotation mechanism to refer to the syntactic value of an expression; and an evaluation mechanism to refer to the value of the expression represented by a syntactic value. We present and compare two approaches, based on instances of a syntax framework, to formalize a syntax-based mathematical algorithm in a formal theory T. In the first approach the syntactic values for the expressions manipulated by the algorithm are members of an inductive type in T, but quotation and evaluation are functions defined in the metatheory of T. In the second approach every expression in T is represented by a syntactic value, and quotation and evaluation are operators in T itself.

cs.LO↗