Go backward to Variable Declarations
Go up to Top
Go forward to Eager Evaluation Semantics

Eager Evaluation Semantics

Without variable declarations:
- [[pi |- I=E: {I:theta}]] $e$ $s$ = {I = [[pi |- E: theta]] $e$ $s$ }
- [[pi |- E₁,E₂: pi₁ U pi₂]] $e$ $s$ =
  ([[pi |- E₁: pi₁]] $e$ $s$ ) union ([[pi |- E₂: pi₂]] $e$ $s$ )
- [[pi |- with $E$ ₁ do $E$ ₂: theta]] $e$ $s$ =
  [[pi -U- pi₁ |- E₂: theta]]( $e$ -U- ([[pi |- E₁: pi₁]] $e$ $s$ )) $s$
- [[pi |- I: theta]] $e$ $s$ = $u$ , where (I= $u$ ) in $e$
- [[pi |- lambdaI:theta₁. E: theta₁ $->$ theta₂]] $e$ $s$ = $f$
  where $f$ $u$ $s'$ =
  [[pi -U- {I:theta₁} |- E: theta₂]]( $e$ -U- {I= $u$ }) $s'$
- [[pi |- E₁ E₂: theta₂]] $e$ $s$ =
  ([[pi |- E₁: theta₁ $->$ theta₂]] $e$ )([[pi |- E₂: theta₁]] $e$ $s$ ) $s$
Type semantics:
- [[{ $i$ :theta_i}_{i in I}]] = ({ $i$ :eval(theta_i) }_{i in
  I})_bottom
- [[theta₁ $->$ theta₂]] = (eval(theta₁) $->$ [[theta₂]])_bottom
- [[comm]] = (Store $->$ Store)_bottom
- [[tauexp]] = (Store $->$ [[tau]])_bottom

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

Id: records.tex,v 1.1 1996/05/20 12:33:10 schreine Exp schreine

Prev

Next