Luca Paolini. Lambda-theories: some investigations. PhD thesis, Università di Genova and Université de la Méditerranée, 2003.

In this thesis we present somes investigations on lambda-calculi, both untyped and typed. The first two parts concerning some pure untyped calculi, while the last concerns PCF and an extension of its syntax.
In the first part, a lambda-calculus is defined, which is parametric with respect to a set Delta of input values and subsumes all the different (pure and untyped) lambda-calculi given in the literature, in particular the classical one and the call-by-value lambda-calculus of Plotkin. It is proved that it enjoys the confluence property, and a necessary and sufficient condition is given, under which it enjoys the standardization property. Hence, we extended some basic syntactical notion of the classical lambda-calculus to the parametric lambdaDelta-calculus such as solvability, separability, theory. We have studied the notions of solvability and separability in the call-by-value setting; unfortunately, there is no evidence on how treat this kind of notions in an unified way for our parametric lambdaDelta-calculus. On the other hand, we are able to show that some property on theories hold for each lambdaDelta-calculus. The notion of solvability in the call-by-value lambda-calculus has been defined and completely characterized, after the preliminary characterization of the class of potentially valuable terms. It turns out that the call-by-value reduction rule (the beta_v-reduction of Plotkin) is too weak for capturing the solvability property of terms, so some new reduction has been defined in order to do this. The notion of separability is the key notion used in the Böhm Theorem, proving that syntactically different beta-eta-normal forms are separable in the classical lambda-calculus endowed with beta-reduction, i.e. in the call-by-name setting. In the case of call-by-value lambda-calculus endowed with beta_v-reduction and eta_v-reduction, it turns out that two syntactically different beta-eta-normal forms are separable too, while the notions of beta_v-normal form and eta_v-normal form are semantically meaningless.
In the second part, the semantics of the parametric lambda-Delta-calculus is considered. A universal operational semantics is given through a reduction machine, parametric with respect to both Delta and a set Theta of output values. It is showed that they can be instantiated in order to give the more interesting operational reduction machines of untyped lambda-calculi. This kind of operational semantics induces theories correct for the related lambda-Delta-calculus. We study some property of the main instances of Delta and Theta. We have defined some parametric notion, as that of relevant contexts, operational extensionality and head-discriminability, hence we try to find some general characterization. It is showed that the standard operational equivalence induced from the Plotkin's call-by-value lambda-calculus is not semisensible, namely there there is a solvable term equated to an unsolvable one. Hence, a syntactical kind of model, said lambda-Delta-interaction model is defined and showed to be fully abstract for the main interesting universal operational semantics. This kind of model is built by introducing the key notion of orthogonality, similar to that used in the Girard's phase semantics and ludics. By mimicking in an awful manner the Girard work, our notion of orthogonality opposes lambda-terms to contexts. Furthermore, we have showed a partial characterization of the orthogonality induced from the evaluation of terms to head normal form, in the classical call-by-name lambda-calculus.
In the last part, we have studied a typed lambda-calculus with constants (PCF-like) and its standard interpretation on coherent spaces and stable functions. It is well-know that the model is not fully abstract with respect to the standard operational semantics, since the Scott-continuous Gustave function. We have showed that in coherent spaces there is some stable function that is not Scott-continuous already in finite domains, thus these functions are independent from that of Gustave that is continuous. Hence, we have extended both the syntax and the operational semantics of the considered language and we have showed that the interpretation of the extended language becomes fully abstract with respect to the standard interpretation on coherent spaces. Thus an operational characterization of stable functions (having domain/codomain on coherent spaces being interpretation on types of the language) is given. After we have developped the results of this part of the thesis, we have discovered that the same problem was considered first by Jim and Meyer, on dI-domains. They have showed some negative results. First they define in a denotational way some stable non-Scott-continuous function similar to our one, hence they show that this operator break-down the coincidence between the applicative-preorder on terms and the contextual-preorder. Finally, they show that with their huge class of ``linear ground operational rules'' defining some PCF-like rules of evaluation, the before considered coincidence, cannot be break-down. So they conclude that it is hard to find an extension of PCF endowed with operators having a meaningful operational description being fully abstract with respect to stable functions. Although, one of the operators that we add to PCF fall down from their PCF-like rules, we think that its meaning is rather clear.

[ bib | http ]

Back