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 fi- nal 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
CARDONE, Felice
2016-01-01
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 fi- nal 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.pdf
Accesso aperto
Descrizione: Articolo principale
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
334.12 kB
Formato
Adobe PDF
|
334.12 kB | Adobe PDF | Visualizza/Apri |
|
Fundamenta Informaticae Volume 149 issue 3 2016 [doi 10.3233%2FFI-2016-1449] Alessi, Fabio; Cardone, Felice -- Tiered Objects.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
370.47 kB
Formato
Adobe PDF
|
370.47 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
