[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Correct use of reduce_nat

I have diefined a Datatype for the Dictionary Problem. 

dictadt[Letter:TYPE]:DATATYPE

  BEGIN
 
   empty: emptydict?
   cons(eow:bool,m:[Letter -> dictadt]): nonemptydict?
 
  END dictadt

Now this Datatype produces this 2 reduce_nat functions:

 reduce_nat(emptydict?_fun: nat, nonemptydict?_fun: [[bool, [Letter ->
nat]] -> nat]): [dictadt -> nat] =
    LAMBDA (dictadt_adtvar: dictadt):
      CASES dictadt_adtvar OF
        empty: emptydict?_fun,
        cons(cons1_var, cons2_var):
            nonemptydict?_fun(cons1_var,
                              LAMBDA (x: Letter):
                                reduce_nat(emptydict?_fun,
                                          
nonemptydict?_fun)(cons2_var(x)))
        ENDCASES;
  
  REDUCE_nat(emptydict?_fun: [dictadt -> nat], nonemptydict?_fun:
[[bool, [Letter -> nat], dictadt] -> nat]):
      [dictadt -> nat] =
    LAMBDA (dictadt_adtvar: dictadt):
      CASES dictadt_adtvar OF
        empty: emptydict?_fun(dictadt_adtvar),
        cons(cons1_var, cons2_var):
            nonemptydict?_fun(cons1_var,
                              LAMBDA (x: Letter):
                                REDUCE_nat(emptydict?_fun,
                                          
nonemptydict?_fun)(cons2_var(x)),
                              dictadt_adtvar)
        ENDCASES;

How can i use one of this function as a measure function ??
I tried the folowing:


retrDictd (d:dictd): RECURSIVE 	Dicta =   
 CASES d OF
  empty: emptyset,
  cons(eow,m): {w:Word | FORALL (l:Letter| member(l,dom(m))):
member(w,add(l,retrDictd(m(l))))}
 ENDCASES  
MEASURE LET a = (LAMBDA (l:Letter),(n:nat): n + 1) IN
       reduce_nat(0, (lambda (b:bool),LAMBDA (l:Letter),(n:nat): n + 1))


But it didnŽ t work ! I know that this function is still not correct
because it wonŽ t produce a Dicta (= set [Word]) but first of all i want
to solve the problem of the measure function !!

PS.: thanks to all who helped me so far !! ( Thanks Thanks )
-- 
---------------------------------------------------------
 ("\''/").__..-''"`-. .         Gernot Lepuschitz
 `9_ 9  )   `-. (    ).`-._.`)gernot@sbox.tu-graz.ac.at 
 (_Y_.)' ._   ) `._`.  " -.-'   Telematik - Student
 ..`-'_..-_/ /-'_.'/               TU - Graz
(l)-'' ((i).' ((!.'              
In the softwarerequirements they said Win95 or better
so I installed Linux.