Le séminaire PPS c'est ce matin 11h!

Bonjour

Nous accueillons aujourd'hui Daniel Leivant (Indiana Univ) qui nous parlera de théorie de systèmes de données.
C'est a 11h dans la salle habituelle 1D23.

Data systems and their intrinsic theories

Given a multi-sorted free algebra A(C) generated by a set C of
constructors, the intrinsic theory for C has as axioms just the closure
conditions of the types of A(C), and their dual (C-induction).  This gets
interesting when we consider equational programs as added axioms.  For
instance, the programs over N that are provably-typed computes exactly the
provably-recursive functions of PA.
We generalize matters from free algebras to *data-systems*, a setting
where inductive and coinductive definitions can be combined at will, and
untyped equational programs can be assigned semantical (= Curry-style)
types.  The intrinsic theory of a data system has closure conditions for
inductive types, with Induction as their dual, and decomposition
conditions for coinductive types, with a suitable notion of Coinduction as
their dual.
We prove a Data-canonicity Theorem, stating that global program-correctness
over all structures, in a Tarskian-semantics sense, is equivalent to
program-correctness in the canonical structure, in the
denotational-semantics sense. We further show that the intrinsic theory
for any non-trivial data-system is mutually interpretable with PA,
regardless of the mix of inductive and coinductive types. We establish a
strong normalization theorem for all intrinsic theories, and consider its
applications.  Finally, we discuss the relation between an intrinsic
theories based on classical vs constructive logic.