Uniform Syntax

Syntax

• Typed language
• Predefined types: bool, int, list (with PROLOG syntax)
• Primitive boolean symbols
  • ~ b (negation),
  • (b1 , b2) (conjunction),
  • (b1 ; b2) (disjunction),
  • (b => e) (guarded expression, meaning: if b then e else undefined),
  • (b => e1 # e2) (conditional, meaning: if b then e1 else e2),
  • (e1 = e2), (e1 ~= e2) (equality / disequality).

Semantics

• Operational semantics: Narrowing (see Hanus 94)
• Declarative Semantics Least Herbrand model characterization

  Computed as the least fixpoint of an interpretation transformer, even in the presence of higher order, lazy evaluation, negation, constraints or default rules

  Bosco et al 87, Moreno-Navarro, Rodríguez-Artalejo 88, 92, González, Hortalá, Rodríguez-Artalejo 90, López-Fraguas 92, Moreno-Navarro 94

Go to index