We investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects.

Tiered Objects

Alessi, Fabio;
2016

Abstract

We investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects.
File in questo prodotto:
File Dimensione Formato  
tiered-pubblicato.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 370.47 kB
Formato Adobe PDF
370.47 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
tiered.pdf

accesso aperto

Descrizione: post-print
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 305.52 kB
Formato Adobe PDF
305.52 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/1134859
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact