perm filename HOMEW2[206,LSP] blob sn#482119 filedate 1979-10-16 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00003 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 .REQUIRE "206MAC.PUB[206,LSP]" source_file C00003 00003 .hd206 FALL 1979 C00008 ENDMK C⊗; .REQUIRE "206MAC.PUB[206,LSP]" source_file; . .odd heading(,,{page}) ; .even heading({page}, , ) ; . .LSPFONT .basicops . .allops .itemmac 1; . .PORTION MAINPORTION .hd206 FALL 1979 .PAGE ← 1 .hw 2, |Oct. 29| .begin .indent 0,3 .item ← 0 .bb More about append. #. Prove the following cancellation rules for ⊗append: .begin nofill ##. ∀u v w:[ [u*w=v*w]≡[u=v] ] ##. ∀u v w:[ [w*u=w*v]≡[u=v] ] .end .bb Rightwing lists. #. Recall that when restricted to lists the operations ⊗car, ⊗cdr and ⊗cons behave unsymmetrically. Thus it is easy to get the first (left most) element of a list and the rest of the list. Often one would like to work on the other end of a list. ##. Write programs to compute the functions ⊗rac, ⊗rdc and ⊗snoc, where for non-empty lists ⊗uu, ⊗rac[uu] is the last element, ⊗rdc[uu] is the list obtained by removing the last element, and for a list ⊗u, and an S-expression ⊗x, ⊗snoc[u,x] adds ⊗x to the end of the list ⊗u. Use only ⊗car, ⊗cdr, ⊗cons and recursive defintion. ##. Give axioms characterizing the functions ⊗rac, ⊗rdc and ⊗snoc representing your programs. The functions ⊗rac, ⊗rdc, ⊗snoc have the following properties .begin nofill indent 8,8 (i) ⊗rac of a non-empty list is an S-expression, (ii) ⊗rdc of a non-empty list is an list, (iii) ⊗snoc of a list and an S-expression is a non-empty list, (iv) the ⊗rac of the ⊗snoc of a list, ⊗u, and an S-expression, ⊗x, is ⊗x, (v) the ⊗rdc of the ⊗snoc of a list, ⊗u, and an S-expression, ⊗x, is ⊗u, and (vi) for a non-empty list ⊗uu, ⊗snoc of the ⊗rdc and the ⊗rac of ⊗uu is just ⊗uu. .end ##. Give domain/range specifications and axioms formallizing the above properties of ⊗rac, ⊗rdc and ⊗snoc. ##. Prove that your programs satisfy these specifications (using the axioms for the representation of the programs as functions). .bb Splitting lists. #. A pair of lists ⊗⊗[v_._w]⊗ is said to split a list ⊗u (⊗⊗Issplit[v,w,u]⊗) if ⊗⊗v*w=u⊗. Write a program ⊗splits[u] that computes a list containing exactly those pairs of lists that split the list ⊗u. Give a sentence that defines the relation ⊗Allsplits[w,u], characterizing the list ⊗w of all splits of a list ⊗u and show that your program is correct with respect to this specification. .end