Fracterm Calculus for Partial Meadows

Fuente: arXiv
Guardado en:
Detalles Bibliográficos
Autores principales: Bergstra, Jan A., Ponse, Alban
Formato: Preprint
Publicado: 2025
Materias:
Acceso en línea:
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
_version_ 1866914561977745408
author Bergstra, Jan A.
Ponse, Alban
author_facet Bergstra, Jan A.
Ponse, Alban
contents Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski semantics. The propositional part of this logic is also known as McCarthy calculus and has been studied extensively. Axioms for the fracterm calculus of partial meadows are given. The case is made that in this way a rather natural formalisation of fields with division operator is obtained. It is noticed that the logic thus obtained cannot express that division by zero must be undefined. An interpretation of the three-valued sequential logic into $\bot$-enlargements of partial algebras is given, for which it is concluded that the consequence relation of the former logic is semi-computable, and that the $\bot$-enlargement of a partial meadow is a common meadow.
format Preprint
id arxiv_https___arxiv_org_abs_2502_13812
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Fracterm Calculus for Partial Meadows
Bergstra, Jan A.
Ponse, Alban
Logic in Computer Science
03C90
F.3.1; F.3.2
Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski semantics. The propositional part of this logic is also known as McCarthy calculus and has been studied extensively. Axioms for the fracterm calculus of partial meadows are given. The case is made that in this way a rather natural formalisation of fields with division operator is obtained. It is noticed that the logic thus obtained cannot express that division by zero must be undefined. An interpretation of the three-valued sequential logic into $\bot$-enlargements of partial algebras is given, for which it is concluded that the consequence relation of the former logic is semi-computable, and that the $\bot$-enlargement of a partial meadow is a common meadow.
title Fracterm Calculus for Partial Meadows
topic Logic in Computer Science
03C90
F.3.1; F.3.2
url https://arxiv.org/abs/2502.13812