perm filename F79[206,LSP] blob sn#485147
filedate 1979-10-24 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00005 PAGES
C REC PAGE DESCRIPTION
C00002 00002 Ideas for exam questions
C00005 00003 Readin
C00006 00004 WRITIN
C00007 00005 PROVIN
Ideas for exam questions
design a representation of floating point numbers which includes
two pieces of information: a mantissa (integer), and an exponent (base 10) (integer).
Using this representation write programs to add, subtract, multiply, divide,
exponentiate, and compare two complex numbers. (Using functions on integers)
Simiilar for fractions, complex numbers.
How about bignums?
Let ⊗rules be a list of "rewriting rules" of the form $$(EQUAL lhs rhs)$.
The $lhs and $rhs components of the rule may have ``pattern variables'' in them.
We say that $lhs matches ⊗e if there is a list of substitutions that can be
made for the pattern variables in $lhs such that the resulting instantiation
is equal to ⊗e.
A rule ⊗r is applicable to ⊗e if the $lhs part of ⊗r matches some subexpression
of ⊗e. Applying ⊗r to ⊗e then consists of replacing that subexpression by
the instantiation of $rhs corresponding to the list of substitutions that
caused $lhs to match at this point.
The program ⊗rewrite[e,rules] goes through the list of rules and looks for
one that is applicable to ⊗e. If one is found it is applied,
and rewrite is applied again to the "simplified" expression using the
same set of rules. If no applicable rules are found ⊗e is returned.
Write interpreter for flograph programs: takes pgm and interpretation of symbols
and input for pgm. Computes output.
Representation of hereditarily finite sets (of atoms) and operations thereon.
set-equality, union, pairing, difference,
list of KPU axioms to be satisfied
#. Show that ⊗mapcar commutes with ⊗reverse and ⊗append. Officially we don't
have a way to reason about programs taking functions as arguments. However,
if we replace ⊗mapcar by a function schema, ⊗mapper, involving a function
parameter ⊗F, then we can give a proof schema, which will provide a proof
for any particular instance of ⊗mapper obtained by choosing a particular function
for ⊗F. Thus
⊗⊗⊗∀u.mapper u=qif qn u qthen qNIL qelse [F qa u_._mapper[qd u]]⊗
and you are to prove
##. ⊗⊗∀u v.[mapper u*v=mapper u*mapper v]⊗
##. ⊗⊗∀u.[mapper reverse u=reverse mapper u]⊗
sequential prog→rec defn
fn for each statement
optimize on second pass
fringe→flat→flatagin for example
modify program to return more infor about what it did
convert f[x]←qt[f,x] to ff[x,n]←if n=0 then error else qt[λx.ff[x,n-1],x]