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