Advertisement

An algebraic interpretation of the λβK-calculus and a labelled λ-calculus

  • Jean-Jacques Levy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 37)

Abstract

The interpretation <I, N>, although strongly inspired by Scott's theory of computation, is purely algebraic. Here, we do not have a definition of application as in Scott [10,11] or Welch [15]. But with the help of the labelled calculus, any expression can be considered as the limit of expressions having a normal form. If we think of λ-expressions as programs, the interpretation <I,N> seems to be the minimal one to consider.Thus we expect that <I,N> is some kind of free interpretation.This is proved by Welch for “continuous semantics”,i.e. roughly speaking for interpretations where the Wadsworth theorem is true.Welch did it for his model but his interpretation seems to be equivalent to the one we used here. Hyland [4 ],who independently considered also the same interpretation, proved that there is an extensional equivalence relation corresponding to equality in I. Furthermore, he showed for any λ-expressions M,M′ that M ⊂ M′ iff M ⊂/Pω M′ where Pω is Scott's model [11]. Another question is to take into account extensionality and build an algebraic interpretation where the η-rule is valid.This is done by Hyland [4 ] Finally,the labelled λ-calculus seems interesting in itself [6 ],since we can capture the history of any reduction in the labels.

Keywords

Normal Form Abstraction Form Lambda Calculus Directed Subset Algebraic Interpretation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Barendregt H.P.,“Some extensional term models for combinatory logics and lambda-calculi”,PhD thesis,Utrecht(1971)Google Scholar
  2. [2]
    Church A.,“The calculi of lambda conversion”,Annals of Math.Studies,n∘6, Princeton(1941)Google Scholar
  3. [3]
    Curry H.B.,Feys R.,“Combinatory logic”,Vol 1,North Holland(1958)Google Scholar
  4. [4]
    Hyland M.,to appear in the Rome conference(1975)Google Scholar
  5. [5]
    Lévy J-J.,“Réductions sures dans le lambda calcul”,3ℴ cycle,Univ of Paris(1974)Google Scholar
  6. [6]
    Lévy J-J.,“Réductions sures et optimales dans le lambda calcul”,to appearGoogle Scholar
  7. [7]
    Milner R.,“Processes;A model of computing agents”,Univ. of Edinburgh,Internal report(1973)Google Scholar
  8. [8]
    Morris J.H.,“Lambda calculus models of programming languages”,PhD thesis, MIT,Cambridge(1968)Google Scholar
  9. [9]
    Nivat M.,“Sur l'interprétation des shémas de programmes monadiques”,Rapport IRIA-LABORIA (1972)Google Scholar
  10. [10]
    Scott D.,“Continuous lattices”,Technical monograph,PRG-7,Oxford(1971)Google Scholar
  11. [11]
    Scott D.,“Data types as lattices”,to appear in Springer Lectures NotesGoogle Scholar
  12. [12]
    Vuillemin J.,“Syntaxe,sémantique et axiomatique d'un langage de programmation simple”,Thèse d'état,Univ. Paris 7(1974)Google Scholar
  13. [13]
    Wadsworth C.P.,“Semantics and pragmatics of the lambda calculus”,PhD thesis, Oxford (1971)Google Scholar
  14. [14]
    Welch P.,“Another problem of lambda calculus”,Univ. of Kent,Private communication (1973)Google Scholar
  15. [15]
    Welch P.,to appear in the Rome conference (1975)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1975

Authors and Affiliations

  • Jean-Jacques Levy
    • 1
  1. 1.IRIA-LaboriaRocquencourtFrance

Personalised recommendations