Toward a geometric view on computations

Philippe Audebaud 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We interpret Intersection Types as the closed sets of some Zariski topology on pure lambda-terms. In this view, the parallel or operator introduced by Boudol is the multiplication for an underlying ring structure. We propose a new calculus which extends pure $\lambda$-calculus along the same lines as relative numbers $Z$ extend natural numbers , the ring operations expressing computation rules on terms. Thus, types are interpreted as the zeros sets for some notion of polynomial ideals (algebraic sets). Terms properties (strong normalisation, confluence, full abstraction) are investigated. Among similarities with Algebraic Geometry, we suggest that terms of interest, such as normalising terms or convergent programs are rare; divergence is a generic property for programs.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070515
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 8:44:06 PM
Last modification on : Saturday, January 27, 2018 - 1:31:31 AM
Long-term archiving on: Sunday, April 4, 2010 - 9:23:08 PM

Identifiers

  • HAL Id : inria-00070515, version 1

Collections

Citation

Philippe Audebaud. Toward a geometric view on computations. RR-5492, INRIA. 2005, pp.16. ⟨inria-00070515⟩

Share

Metrics

Record views

193

Files downloads

115