Checked corecursive streams are a novel approach to stream definitions relying on a semantics of function application detecting cyclic calls, and a well-definedness check ensuring that access to an arbitrary index will always return a result. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme. We show that this actually enhances expressive power, since the interleaving operator cannot be expressed by the others, and that it is still possible to perform a sound and complete well-definedness check, through a symbolic computation which mimics access to an arbitrary index.

Checked corecursive streams: Expressivity and completeness

Ancona D.;Barbieri P.;Zucca E.
2023-01-01

Abstract

Checked corecursive streams are a novel approach to stream definitions relying on a semantics of function application detecting cyclic calls, and a well-definedness check ensuring that access to an arbitrary index will always return a result. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme. We show that this actually enhances expressive power, since the interleaving operator cannot be expressed by the others, and that it is still possible to perform a sound and complete well-definedness check, through a symbolic computation which mimics access to an arbitrary index.
File in questo prodotto:
File Dimensione Formato  
journal-final.pdf

accesso chiuso

Tipologia: Documento in versione editoriale
Dimensione 597.93 kB
Formato Adobe PDF
597.93 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.

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