Abstract:

This presentation proposes a new semantical model for LOTOS data types, based on explicit distinction between constructors and functions and a deterministic evaluation function. This results in effectively computable data types and enhances modularity. We also define an associated type definition syntax, inspired from ML, and present some possible developments. We then discuss how equality can be defined: though some types (like sets) cannot be defined so that language-level equality matches the intended equivalence, quite convenient workarounds can be used. We show how the deterministic evaluation allows simpler specifications, and how modularity and abstractness can be enforced. Finally, we will address the compatibility of the proposed evaluation with existing simulation approaches like rewriting and narrowing.