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

## 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## Preview

Unable to display preview. Download preview PDF.

## References

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