Nuprl Definition : longest-prefix

longest-prefix(P;L) ==
fix((λlongest-prefix,P,L. if null(L)
then []

                           else let p = longest-prefix (λL'.(P [hd(L) / L'])) tl(L) in

                                    if null(p)
                                    then if null(tl(L)) then []
                                         if P [hd(L)] then [hd(L)]
                                         else []
                                         fi
                                    else [hd(L) / p]
                                    fi
                           fi ))
  P
  L

Definitions occuring in Statement : hd: hd(l), null: null(as), tl: tl(l), cons: [a / b], nil: [], ifthenelse: if b then t else f fi , let: let, apply: f a, fix: fix(F), lambda: λx.A[x]
Definitions occuring in definition : fix: fix(F), let: let, lambda: λx.A[x], null: null(as), tl: tl(l), ifthenelse: if b then t else f fi , apply: f a, nil: [], cons: [a / b], hd: hd(l)
FDL editor aliases : longest-prefix

Latex:
longest-prefix(P;L) == fix((\mlambda{}longest-prefix,P,L. if null(L) then [] else let p = longest-prefix (\mlambda{}L'.(P [hd(L) / L'])) tl(L) in if null(p) then if null(tl(L)) then [] if P [hd(L)] then [hd(L)] else [] fi else [hd(L) / p] fi fi )) P L Date html generated: 2016_05_15-PM-03_26_06 Last ObjectModification: 2015_09_23-AM-07_43_14 Theory : general Home Index