Mathematical Semantics for Higher Order Programming Languages

摘要

Complete operational and mathematical semantics are presented for a higher order applicative algorithmic language (BAL). Both semantics involve partially ordered domains closed under limits of convergent sequences. Procedure calls are formalized via lambda calculus reductions, or copy rule. Evaluations involve a more general form of computability described as nondeterministic computability. The mathematical semantics is obtained via embeddings in reflexive domains. Both semantics are proved to be equivalent, and several applications are given. The adequacy of the copy rule is proved in standard situations where computability is deterministic. Several examples are presented. (Author)