Nuprl Definition : cpsquicksort

cpsquicksort(cmp;L;k) ==
  fix((λcpsquicksort,L,k. if null(L)
                         then k L
                         else let x = hd(L) in
                               let L1 = filter(λz.0 <z cmp z x;L) in
                               let L2 = filter(λz.(0 =z cmp x z);L) in
                               let L3 = filter(λz.0 <z cmp x z;L) in
                               cpsquicksort L1 (λS1.(cpsquicksort L3 (λS3.(k (S1 @ L2 @ S3)))))
                         fi )) 
  L 
  k


Definitions occuring in Statement :  hd: hd(l),  null: null(as),  filter: filter(P;l),  append: as @ bs,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  let: let,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  ifthenelse: if b then t else f fi ,  null: null(as),  hd: hd(l),  eq_int: (i =z j),  let: let,  filter: filter(P;l),  lt_int: i <z j,  natural_number: $n,  lambda: λx.A[x],  apply: f a,  append: as @ bs
FDL editor aliases :  cpsquicksort
Latex:
cpsquicksort(cmp;L;k)  ==
    fix((\mlambda{}cpsquicksort,L,k.  if  null(L)
                                                  then  k  L
                                                  else  let  x  =  hd(L)  in
                                                              let  L1  =  filter(\mlambda{}z.0  <z  cmp  z  x;L)  in
                                                              let  L2  =  filter(\mlambda{}z.(0  =\msubz{}  cmp  x  z);L)  in
                                                              let  L3  =  filter(\mlambda{}z.0  <z  cmp  x  z;L)  in
                                                              cpsquicksort  L1  (\mlambda{}S1.(cpsquicksort  L3  (\mlambda{}S3.(k  (S1  @  L2  @  S3)))))
                                                  fi  )) 
    L 
    k


Date html generated: 2016_05_15-PM-04_28_55
Last ObjectModification: 2015_09_23-AM-07_48_49

Theory : general


Home Index