PDF Archive

Easily share your PDF documents with your contacts, on the Web and Social Networks.

Share a file Manage my documents Convert Recover PDF Search Help Contact



624 TermPaper .pdf



Original filename: 624_TermPaper.pdf

This PDF 1.5 document has been generated by TeX / pdfTeX-1.40.15, and has been sent on pdf-archive.com on 30/11/2015 at 18:47, from IP address 157.245.x.x. The current document download page has been viewed 597 times.
File size: 155 KB (6 pages).
Privacy: public file




Download original PDF file









Document preview


624: Bootstrappers guide: A Practical approach
Roscoe S. Casita
November 30, 2015

1

This problem-solution implementation oriented guide to bootstrapping
a programming language, specifically λ through a C# backend. Simple
lazily evaluated untyped λ calculus as per [Horwitz, 2010] is the target language. Two extensions to the standard grammar are added to support left
hand recursion, and macro-aliasing to support statements such as {T RU E =
λx.λy.x}. The proof in the pudding is showing that {P RED(SU CC(ZERO))}
is indeed {ZERO}.

Axiom-Semantics: Implementation via Code, structures, and text.
Lexical Parser: Add text as regular-rule which consumes lexical text.
Syntactic Parser: Add text as grammar-rule for Parsing-Engine.
Parsing-Engine: Use rules to decompose text into a syntax-tree of tokens.
Convert: Transform syntax-tree of tokens into an expression-tree of
[λ Abstraction or Macro or Variable or Application]. This is
intrinsically dependent upon the grammar-rules and Interpreter.
Interpreter-Step: Switch on type of expression-tree:
Variable → Variable, done
Abstraction → Abstraction, done
Apply (Exp1’ ,Exp2 ) → Apply (Exp1’ ,Exp2 ), done
Macro (replacement-exp) → replacement-exp, notdone
Apply (Exp1 ,Exp2 ) → Apply ( Exp1’ ,Exp2 ), notdone
Apply (Abst(Var ,Body ),Exp) → β ↓ Body [Exp/Var ], notdone
Interpreter-Step recursively evaluates Exp1 of Apply {Exp1 ,Exp2 }
until one step is taken then notdone or no progress done. Thus lazy
evaluation is in not evaluating Exp2 . [Harold Abelson, 1996]
Running a Program: Here control is returned to the user. As each step is
a total transformation of exp-tree to exp-tree’ , the user will need to
handle unexpected results. Basic syntax errors are handled upstream
before interpretation begins. Debugging of core semantics at run time
is supported through the IDE. Facilities are embedded in the top level
system to allow Run-until-done to be performed. User beware.

2

The tightly coupled dependency and relationship between each phase of
transformation cannot be over stated. Thus each transform stage depends
upon the knowledge of output from the last stage and knowledge of expected
input in the next stage.

1

Stage 1: Grammar Loading Parsing

The parser contains two axioms for creating Rules:
text as reg-exp can be added to a List of reg-rule.
text as grammar-rule can be added to a List of grammar-rules.
Thus a version of Juxtaposition and Alternation [Neighbors, 2015] is implemented via multiple rules. Rule addition order controls parsing ordering.

2

Stage 2: Lexical Decomposition

The parser exposes a parse program routine that accepts text, and returns
text + syntax-tree. Starting with the topmost PROGRAM rule, the
LL(*) recursive decent parser expands each rule (preserving input at each
stage), adding the rule to the tree if it found, and restoring input if no
match was generated. [Alfred V. Aho, 1988], [Parsons, 1992] Thus if a
parse fails, the input text will start with the first character not matched.
This is implemented via recursive functions Parse and Parse-Segment
called from a top level wrapper Parse-Program.

3

Stage 3: Transform Syntax to Exp-tree

Intimate knowledge of the grammar definition is utilized in this function to
match a rule via switch statement to execute the appropriate expressiontree building Code. Left associativity via <EXPLIST > and the handlers
for-loop is a prime example of the intricate interconnected relationships.
Free Variable capture is handled during this stage with a heap of {text,Var }
relationships. Abstraction will push Variable before proceeding, and pop
after returning from the recursive call. Any syntactic Variable inside the
Body will be pulled from the heap otherwise a new free Variable is created.
Macro definitions are added to the hyper-static Macro-environment for
lookup later, no exp-tree is returned as the program is done.
3

4

Stage 4: Interpret Step of expression-tree

This lambda-interpreter implements the following core semantic operations:

done States:

Var
x→x

Abstraction
λ→λ

Apply Done
e10 , e2 → e10 , e2

notdone States:

Apply Reduce β
λx.e1, e2 → e1[e2/x]

Apply Left
e1, e2 → e10 , e2

Macro
X.e → e

Interpretation ends if the Apply cannot reduce further. This control
shunting by single step allows incrementally advancing {(λx.x)(λy.yy)(λz.zz)}
via external user control. This will infiniantly recourse but in a externally
controlled manner. The machine will predictably halt with the symbol done
or notdone on all valid exp-trees. Notice the program cannot predictably
return done.

5

Stage 5: Loop Until Debug

Full evaluation of a program is while(!done) {exp = Interpret(exp)}.
Introduction of external control is handled easily as Interpret-Step takes
a maximum of one tree transformation per step. Specifically textual tape
and pictorial tape can be generated and displayed for inspection. Runtime
debugging facilities are either implemented in the interpreter or inside the
interpretation. Neither are for the faint of heart. [Queinnec, 1994]

6

After Thoughts and Explorations

This exercise was exceptionally complicated, convoluted, and enlightening.
There most incomplete portion of this system is enough test cases to demonstrate working as intended.
Ultimately the program found in the appendix was run on the system
generating the lazy evaluation proof reduction tree. Evaluation of the problem on paper could have been solved with less then an hour of work. 100
hours to generate automated proof trees is an obvious savings in time. Lazy
evaluation of the problem statement generated work instead of reducing.
4

7

Appendix

Grammar Regex: @”ˆ(?<NAME>< \ w+>)::==(?<RULE>(< \w+> |\w+))+”
Regular Regex: @”ˆ(?<NAME> [A-Z][A-Z 0-9]*):=(?<EXPRESSION> \ˆ.*)”
Final derivation of ISZERO (PRED (SUCC ZERO)) TRUE:
TRUE= λx.λy.x
FALSE=λx.λy.y
ISZERO = λl.l(λh.λt.FALSE)
PRED = λl.l FALSE
SUCC = λl.(λh.λt.(λs.s h t)) f l
ZERO = λx.λy.y
ISZERO (PRED (SUCC ZERO)) TRUE
λl.l λh.λt.FALSE (PRED (SUCC ZERO)) TRUE
PRED (SUCC ZERO) λh.λt.FALSE TRUE
λl.l FALSE (SUCC ZERO) λh.λt.FALSE TRUE
SUCC ZERO FALSE λh.λt.FALSE TRUE
λl.λh.λt.λs.s h t f l ZERO FALSE λh.λt.FALSE TRUE
λh.λt.λs.s h t f ZERO FALSE λh.λt.FALSE TRUE
λt.λs.s f t ZERO FALSE λh.λt.FALSE TRUE
λs.s f ZERO FALSE λh.λt.FALSE TRUE
FALSE f ZERO λh.λt.FALSE TRUE
λx.λy.y f ZERO λh.λt.FALSE TRUE
λy.y ZERO λh.λt.FALSE TRUE
ZERO λh.λt.FALSE TRUE
λx.λy.y λh.λt.FALSE TRUE
λy.y TRUE
TRUE
λx.λy.x
TRUE

5

References
[Alfred V. Aho, 1988] Alfred V. Aho, Ravi Sethi, J. D. U. (1988). Compilers: Principles, techniques, and tools.
[Casita, 2015a] Casita, R. S. (2015a). Grammar parser. http://pastebin.
com/HfSpJVNu.
[Casita, 2015b] Casita, R. S. (2015b).
pastebin.com/SBeiBCCj.

Lambda grammar.

http://

[Casita, 2015c] Casita, R. S. (2015c).
pastebin.com/UpaJQJ5r.

Lambda interpreter.

http://

[Casita, 2015d] Casita, R. S. (2015d). Lamda proof of pred ( succ zero) is
zero. http://pastebin.com/iFR30kZC.
[Casita, 2015e] Casita, R. S. (2015e). Top level loop. http://pastebin.
com/R2ZawHm0.
[Harold Abelson, 1996] Harold Abelson, Gerald Jay Sussman, J. S. (1996).
Structure and interpretation of computer programs.
[Horwitz, 2010] Horwitz, S. B. (2010). Cs704. http://pages.cs.wisc.
edu/~horwitz/CS704-NOTES/2.LAMBDA-CALCULUS-PART2.html.
[Neighbors, 2015] Neighbors, J. M. (2015).
Meta ii.
bayfronttechnologies.com/mc_tutorial.html.

http://www.

[Parsons, 1992] Parsons, T. W. (1992). Compiler construction.
[Paulson, 2000] Paulson, L. (2000). Ml for the working programmer.
[Queinnec, 1994] Queinnec, C. (1994). Lisp in small pieces.

6


Related documents


624 termpaper
presentation
cdsyllabus
cdunit2
cdunit4
flatunit4


Related keywords