Nuprl Definition : quicksort

quicksort(cmp;L) ==
  fix((λquicksort,L. if null(L)
                    then 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 (quicksort L1) @ L3 @ (quicksort L2)
                    fi )) 
  L


Definitions occuring in Statement :  hd: hd(l),  null: null(as),  filter: filter(P;l),  append: as @ bs,  callbyvalueall: callbyvalueall,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  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),  lt_int: i <z j,  callbyvalueall: callbyvalueall,  filter: filter(P;l),  lambda: λx.A[x],  eq_int: (i =z j),  natural_number: $n,  append: as @ bs,  apply: f a
FDL editor aliases :  quicksort
Latex:
quicksort(cmp;L)  ==
    fix((\mlambda{}quicksort,L.  if  null(L)
                                        then  L
                                        else  let  x  \mleftarrow{}{}  hd(L)
                                                  in  let  L1  \mleftarrow{}{}  filter(\mlambda{}z.0  <z  cmp  z  x;L)
                                                        in  let  L2  \mleftarrow{}{}  filter(\mlambda{}z.0  <z  cmp  x  z;L)
                                                              in  let  L3  \mleftarrow{}{}  filter(\mlambda{}z.(0  =\msubz{}  cmp  x  z);L)
                                                                    in  (quicksort  L1)  @  L3  @  (quicksort  L2)
                                        fi  )) 
    L


Date html generated: 2016_05_15-PM-04_28_13
Last ObjectModification: 2015_09_23-AM-07_48_43

Theory : general


Home Index