Two preprints on Second-Order Algebraic Structure.

Two preprints on Second-Order Algebraic Structure.

[Marcelo Fiore]

Two extended abstracts on

      (1) Second-Order Equational Logic 
and
      (2) Second-Order Algebraic Theories

are available as follows.

We'd be grateful for any comments, 
Marcelo.


--------

(1) M.Fiore and C.-K.Hur.  Second-Order Equational Logic.

      <http://www.cl.cam.ac.uk/~mpf23/papers/Types/soeqlog.pdf>

      To appear in Proceedings of the 19th EACSL Annual Conference on
      Computer Science Logic (CSL 2010), 2010.

      Abstract.  We extend universal algebra and its equational logic from
      first to second order as follows.

        1. We consider second-order equational presentations as specified by
  	 identities between second-order terms, with both variables and
  	 parameterised metavariables over signatures of variable-binding
           operators.

        2. We develop an algebraic model theory for second-order equational
  	 presentations, generalising the semantics of (first-order)
  	 algebraic theories and of (untyped and simply-typed) lambda
           calculi.

        3. We introduce a deductive system, Second-Order Equational Logic,
  	 for reasoning about the equality of second-order terms.  Our
  	 development is novel in that this equational logic is synthesised
           from the model theory.  Hence it is necessarily sound.

        4. Second-Order Equational Logic is shown to be a conservative
           extension of Birkhoff’s (First-Order) Equational Logic.

        5. Two completeness results are established: the semantic
  	 completeness of equational derivability, and the derivability
  	 completeness of (bidirectional) Second-Order Term Rewriting.


(2) M.Fiore and O.Mahmoud.  Second-order algebraic theories.

      <http://www.cl.cam.ac.uk/~mpf23/papers/Types/soat.pdf>

      To appear in Proceedings of the 35th International Symposium on
      Mathematical Foundations of Computer Science (MFCS 2010), 2010.

      Abstract.  Fiore and Hur recently introduced a conservative extension
      of universal algebra and equational logic from first to second order.
      Second-order universal algebra and second-order equational logic
      respectively provide a model theory and a formal deductive system for
      languages with variable binding and parameterised metavariables.  This
      work completes the foundations of the subject from the viewpoint of
      categorical algebra.  Specifically, the paper introduces the notion of
      second-order algebraic theory and develops its basic theory.  Two
      categorical equivalences are established: at the syntactic level, that
      of second-order equational presentations and second-order algebraic
      theories; at the semantic level, that of second-order algebras and
      second-order functorial models.  Our development includes a
      mathematical definition of syntactic translation between second-order
      equational presentations.  This gives the first formalisation of
      notions such as encodings and transforms in the context of languages
      with variable binding.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]