Logic in Computer Science (LICS 1993)

Paper: Non-determinism in a functional setting (at LICS 1993)

Authors: C.-H. Luke Ong

Abstract

The pure untyped lambda calculus augmented with an (erratic) choice operator is considered as an idealised nondeterministic functional language. Both the `may' and the `must' modalities of convergence are of interest. Following Abramsky's (1991) work on domain theory in logical form, we identify the denotational type that captures the computational situation δ=P[[δ→δ]⊥], where P[-] is the Plotkin power-domain functor. We then carry out a systematic programme that hinges on three distinct interpretations of δ, namely process-theoretic, denotational, and logical. The main theme of the programme is the complementarity of the various interpretations of δ. This work may be seen as a step towards a rapprochement between the algebraic theory of processes in concurrency on the one hand, and the lazy lambda calculus as a foundation for functional programming on the other

BibTeX

  @InProceedings{Ong-Nondeterminisminafu,
    author = 	 {C.-H. Luke Ong},
    title = 	 {Non-determinism in a functional setting},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {275--286},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }