User loginNavigation 
CMachineI semiformalized some part of the translation process for a compiler I am working on. I need people, to do my homework, to shoot as many holes in it as possible, and possibly supply references. I am aware of Thompsons work, but I'll admit I never really got past his elaborate notation. Below a convenience notation I use. Please read it as a preview. I could have done it shorter, the full notation and evaluation process is elaborated as you read. I should rewrite it such that it introduces the full notation in a few paragraphs. Excuses for that. A DOT Evaluator Note that there is nothing new about this notation. It is a machineamiable convenience notation used to show, with a few invariants, that it is possible to safely translate combinatorial expressions to C, not as a new notation for combinatorics. A DOT expression is a syntactic notation for standard combinatorial expressions. A combinatorial DOT expression consists of constants, variables written in lower case, dots '.', combinators in uppercase, and series of squared series out of the former four. A rewrite rule is a squared series starting with a combinator producing a combinator expression, bound variables may occur in rewrites. Examples:
(What is the expression for lazy evaluation of S?) Basic Rewrite Rules A DOT evaluator rewrites a combinator with a fixed strategy. Always, the last expression in a series is evaluated. When it reduces to a constant, its value is placed in the first notnested dot encountered reading from righttoleft. When it reduces to a squared series, that squared series replaces the original term. Evaluation halts when the last expression does not reduce. The above rewriter gives a fixed rewrite strategy on DOT expressions. Note that the order of the series rewritten to matters. Example, using some extra notation:
Evaluation of F 3:
Expand and apply rules. The above rewrite rules are not complete. Reducing a combinator also implies that all extra arguments are inherited by the first squared expression of the series reduced to. Also, a Curried expression is treated as a constant. Dots or variables may not occur in the first position, rather, a special apply @ combinator is used where [@ v] = v, in case the v held a squared expression. In the rules above, the apply is implicit. I.e., the rewrite for I should be read as [I x] = [@ x]. Examples:
also,
Wellformedness and complete reduction All variables occurring on the righthand side must be bound on the lefthand side of a rewrite. In the righthandside of a rewrite, a squared expression must be bound to an exclusive dot to its right, there may not be more dots than squared expressions. All squared expression either start with a combinator followed by arguments, or hold one constant. Since a rewrite substitutes all variables, no variables will occur when rewriting a term which doesn't contain variables; a term without variables will therefore rewrite to another term without variables. Since the last term, during the rewriting of a dot expression, cannot contain dots, since all dots in the last term will always be filled, terms rewritten are always strongly reduced. Since all terms rewritten to always start with a combinator, albeit apply, all squared terms always start with a combinator. The above invariants are sufficient to guarantee that each combinator can be compiled directly to a C routine, and that, by the confluency lemma, terms who have a normal form reduce to that. (I guess.) (I should show Turing equivalence here.) Shift/Reset For example (check with compiler internals):
By marco at 20100614 13:48  LtU Forum  previous forum topic  next forum topic  other blogs  4940 reads

Browse archivesActive forum topics 
Recent comments
11 hours 7 min ago
21 hours 49 min ago
1 day 5 hours ago
1 day 6 hours ago
1 day 8 hours ago
1 day 9 hours ago
1 day 10 hours ago
1 day 10 hours ago
1 day 16 hours ago
1 day 19 hours ago