Go backward to Typing of Parameter Lists
Go up to Top
Go forward to Lambda Abstraction Principle

Semantics of Parameter Lists

Defined via semantics of declarations:
Abstraction:
- [[pi |- define I(F)=U: {I:pi₁ $->$ theta}dec]] $e$ $s$
     = ({I= $p$ }, $s$ )
     where $p$ $e$ ₁ $s$ ₁ =
        [[pi -U- pi₁ |- U: theta]]( $e$ -U- $e$ ₁) $s$ ₁
     and pi₁ = type-attrs(F)
Invocation:
- [[pi |- invoke I(D): theta]] $e$ $s$ = $p$ $e$ ₁ $s$ ₁
  where (e₁, s₁) = [[pi |- D: pi₁dec]] $e$ $s$
  and (I= $p$ ) in $e$
- Store at point of invocation is supplied to actual parameters.
- Abstractions are evaluated lazily, store is ignored.
- Abstractions are evaluated eagerly, store is used.

Correspondence is forced upon language!

Wolfgang.Schreiner@risc.uni-linz.ac.at

Id: parameter.tex,v 1.1 1996/04/25 11:40:48 schreine Exp schreine

Prev

Next