Separating Functional Computation from Relations

Ulysse Gérard 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : The logical foundations of arithmetic generally start with a quantificational logic of relations. Of course, one often wishes to have a formal treatment of functions within this setting. Both Hilbert and Church added to logic choice operators (such as the epsilon operator) in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that does not extend the underlying logic with either choice principles or with an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions
Type de document :
Communication dans un congrès
26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. 82 (23), pp.23:1--23:17, 2017, LIPIcs
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01615683
Contributeur : Ulysse Gérard <>
Soumis le : jeudi 12 octobre 2017 - 16:33:36
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Fichier

CSL_2017_paper_66.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01615683, version 1

Citation

Ulysse Gérard, Dale Miller. Separating Functional Computation from Relations. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. 82 (23), pp.23:1--23:17, 2017, LIPIcs. 〈hal-01615683〉

Partager

Métriques

Consultations de la notice

83

Téléchargements de fichiers

13