Content deleted Content added
Add section: Syntax |
quick sketch of denotational semantics |
||
Line 30:
: ('''nat'''s will be interpreted as booleans here with a convention like zero denoting truth, and any other number denoting falsity)
==Semantics==
<!-- todo: operational semantics -->
===Denotational semantics===
A relatively straightforward semantics for the language is the '''Scott model'''. In this model,
* Types are interpreted as certain [[___domain theory|domains]].
** <math>[[ \textbf{nat} ]] := \mathbb{N}_{\bot}</math> (the natural numbers with a bottom element adjoined, with the flat ordering)
** <math>[[ \sigma \to \tau \, ]]</math> is interpreted as the ___domain of [[Scott-continuous]] functions from <math>[[\sigma]] \,</math> to <math>[[\tau]] \,</math>
* A context <math>x_1 : \sigma_1, \; \dots, \; x_n : \sigma_n</math> is interpreted as the product <math>[[\sigma_1]] \times \; \dots \; \times [[\sigma_n]]</math>
* Terms in context <math>\Gamma \; \vdash \; x \; : \; \sigma</math> are interpreted as continuous functions <math>[[\Gamma]] \; \to \; [[\sigma]]</math>
** Variable terms are interpreted as projections
** Lambda abstraction and application are interpreted by making use of the [[cartesian closed]] structure of the category of domains and continuous functions
** '''Y''' is interpreted by taking the [[least fixed point]] of the argument
This model is not fully abstract for PCF; but it is fully abstract for the language obtained by adding a ''parallel or'' operator to PCF.
| |||