Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi Pavithra,

Your definition for num-of-terms() looks fine. rootsym() however is missing 
basis cases.
I wonder about the usefulness of a-constant?() and a-variable?() since the 
information
encoded in the sorts; still if you want them you can defined them to be 
trivial sort checks.

subterms() is more subtle; it looks like you intend all subterms rather than 
immediate
subterms, and to include the original term itself. You can do it with a 
single operator
that recurses both into the term structure and along arguement lists, with 3 
base cases
and two inductive cases.

Here are the reformulated operators:

fmod NEW-TERM is
  protecting META-LEVEL .

  op a-constant? : Term -> Bool .
  eq a-constant?(T:Term) = T:Term :: Constant .

  op a-variable? : Term -> Bool .
  eq a-variable?(T:Term) = T:Term :: Variable .

  op rootsym : Term -> Qid .
  eq rootsym(C:Constant) = C:Constant .
  eq rootsym(V:Variable) = V:Variable .
  eq rootsym(Q:Qid[TL:TermList]) = Q:Qid .

  op subterms : TermList -> TermList .
  eq subterms(empty) = empty .
  eq subterms(C:Constant) = C:Constant .
  eq subterms(V:Variable) = V:Variable .
  eq subterms(Q:Qid[TL:TermList]) = Q:Qid[TL:TermList], subterms(TL:TermList) 
.
  eq subterms((T:Term, TL:TermList)) = subterms(T:Term), 
subterms(TL:TermList) .
endfm

red upTerm(gcd(X:Nat, 100) + 5 * Y:Nat) .

red a-constant?('0.Zero) .
red a-constant?('s_^5['0.Zero]) .

red a-variable?('0.Zero) .
red a-variable?('Y:Nat) .

red rootsym('0.Zero) .
red rootsym('Y:Nat) .
red rootsym('s_^5['0.Zero]) .

red subterms('_+_['_*_['Y:Nat,'s_^5['0.Zero]],'gcd['X:Nat,'s_^100['0.Zero]]]) 
.

Steven

On Wednesday 14 April 2010, Pavithra Krishnan wrote:
>  Hello
> 
>   I am working on a program that accepts terms which can have any number of
> subterms. I have counted the number of sub terms and I understand meta term
> is the best way to do this. I was wondering if we input terms like
>  f(a,h(a)) or h(h(a)) I can break it into subterms like a,h(a),to the last
>  level down. Is there also a better way to represent each of these as a
>  constant other than the .Constant. I would like to use the Bachmair -
>  Tiwari inference rules on this to check for congruence closure .
> 
>  I have this program which checks for the number of subterms
> 
> fmod NEW-TERM is
>     protecting META-TERM .
>     protecting INT .
>     protecting BOOL .
>     protecting QID .
>     protecting A-LIST{Qid,Int} .
> 
> 
>     sorts Newterm .
> 
>     subsorts Term < Newterm .
> 
>     op c : Nat -> Newterm .
> 
>     var C : Constant .
> 
>     var N : Qid .
> 
>     var T : Term .
> 
>     var L : TermList .
> 
>     op subterms : Term -> TermList .
> 
>     eq subterms(C) = C .
> 
>     eq subterms(N [L]) = N[L], L .
> 
> --- red subterms('g['a.Constant, 'b.Constant]) .
> 
>     op num-of-terms : TermList -> Nat .
> 
>     eq num-of-terms(empty) = 0 .
> 
>     eq num-of-terms(T) = 1 .
> 
>     eq num-of-terms((T, L)) = 1 + num-of-terms(L) .
> 
> --- red num-of-terms(('a.Constant, 'b.Constant)) .
> 
>     op a-constant? : Term -> Bool .
> 
> ---    eq a-constant?(C) = true .
>     ceq a-constant?(N) = true if (getType(N) == 'Constant) .
>     eq a-constant?(T) = false [owise] .
> 
>     op a-variable? : Term -> Bool .
> 
>     ceq a-variable?(N) = true if (getType(N) == 'Variable) .
> 
>     eq a-variable?(T) = false [owise] .
> 
>     op rootsym : Term -> Qid .
> 
>     eq rootsym(N [L]) = N .
> 
> --- red rootsym('g['a.Constant, 'b.Constant]) .
> 
> endfm
> 
> Any input is appreciated
> Thank you
> Pavithra
> 
> --
> Never explain yourself to anyone .A person who likes you doesn't need it
>  and a person who dislikes you will not believe it!!
> People may not believe what you say ,but they will believe what you do !
> The definition for insanity is doing the same thing over and over again and
> expecting the outcome to be suddenly different! if
>