**srlm@ukc.UUCP (S.R.L.Meira)** (06/28/84)

[-: kipple :-] in the hope that many of you are also interested in combinatory logic... please have a look at this and mail me any suggestions, references, etc. ------------------ [by a. pettorossi in notre dame j. form. logic 22 (4) 81] define: marking is a function that assigns, for each combinator in a term (tree) the number of left choices (of path) that one has to make to go from the root to the combinator. ex.: marking SII = <S,2><I,1><I,0> the set right applied subterms of a combinator X is defined as: 1) if X is a basic combinator or a variable ras(X) = {X) 2) if X is (YZ) then ras(YZ) = union (ras(X)) Z a combinator X with reduction axiom X x1 x2 x3 ... xk -> Y has non-ascending property iff for all i, 1<=i<=k, if <xi,p> occurs in marking (X x1...xk) and <xi,q> occurs in marking Y, then p >= q. a combinator (X x1 x2 ... xk -> Y) has compositive effect iff a right applied subterm of Y is not a variable. ------------------ Theorem: given a subbase B={X1,...Xk} such that all Xi in B have non-ascending property and no compositive effect, every reduction strategy applied to any Y in B+ leads to normal form. ------------------ Open Problem: does the theorem hold if non-ascending property is the only condition? ------------------ My personal questions: if one specifies leftmost-outermost reduction only, would the Open Problem be any easier? how much of combinatory logic can we do with B? and with non-ascending property only? silvio lemos meira UUCP: ...!{vax135,mcvax}!ukc!srlm Post: computing laboratory university of kent at canterbury canterbury ct2 7nf uk Phone: +44 227 66822 extension 568