src/HOL/Lambda/ParRed.thy
author nipkow
Mon May 22 14:12:40 1995 +0200 (1995-05-22)
changeset 1124 a6233ea105a4
parent 1120 ff7dd80513e6
child 1126 50ac36140e21
permissions -rw-r--r--
Polished the presentation making it completely definitional.
     1 (*  Title:      HOL/Lambda/ParRed.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TU Muenchen
     5 
     6 Parallel reduction and a complete developments function "cd".
     7 Follows the first two pages of
     8 
     9 @article{Takahashi-IC-95,author="Masako Takahashi",
    10 title="Parallel Reductions in $\lambda$-Calculus",
    11 journal=IC,year=1995,volume=118,pages="120--127"}
    12 *)
    13 
    14 ParRed = Lambda + Confluence +
    15 
    16 consts  par_beta :: "(db * db) set"
    17 
    18 syntax  "=>" :: "[db,db] => bool" (infixl 50)
    19 
    20 translations
    21   "s => t" == "(s,t) : par_beta"
    22 
    23 inductive "par_beta"
    24   intrs
    25     var   "Var n => Var n"
    26     abs   "s => t ==> Fun s => Fun t"
    27     app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    28     beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
    29 
    30 consts
    31   cd  :: "db => db"
    32   deFun :: "db => db"
    33 
    34 primrec cd db
    35   cd_Var "cd(Var n) = Var n"
    36   cd_App "cd(s @ t) = (case s of
    37             Var n => s @ (cd t) |
    38             s1 @ s2 => (cd s) @ (cd t) |
    39             Fun u => deFun(cd s)[cd t/0])"
    40   cd_Fun "cd(Fun s) = Fun(cd s)"
    41 
    42 primrec deFun db
    43   deFun_Var "deFun(Var n) = Var n"
    44   deFun_App "deFun(s @ t) = s @ t"
    45   deFun_Fun "deFun(Fun s) = s"
    46 end