Skip to Content.
Sympa Menu

maude-help - [Maude-help] Break down to smaller terms

maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] Break down to smaller terms


Chronological Thread 
  • From: Pavithra Krishnan <pavithragopi AT gmail.com>
  • To: maude-help AT cs.uiuc.edu
  • Subject: [Maude-help] Break down to smaller terms
  • Date: Wed, 14 Apr 2010 06:22:14 -0400
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help>
  • List-id: <maude-help.cs.uiuc.edu>

 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



Archive powered by MHonArc 2.6.16.

Top of Page