MIT 6.044J/18.423J Handout 23 6.044 Fall 1996 13 December, 1996 Problem Set 5 Solutions by Ozlem Uzuner and A. R. Meyer Handout 14 Problem 1: A variable x has a free occurence in a hole in a -context C if: C is a just a hole, []. C is a conditional, (if ) and x has a free occurence at the hole in one of the subexpressions , or that contains the hole. C is a combination, ( ...) and x has a free occurence at the hole in the (necessarily unique) subexpression , , ,... that contains the hole. C is a lambda expression of the form (lambda () ()), x is not in the and x has a free occurence in the hole in the . C is a body that begins with one or more definitions and an expression. X is free if it is not one of the defined variables and it has a free occurence either in the expression part of one of the definitions or in the expression at the end of the body. Handout 14 Problem 5: A value, V, is a series of zero or more immediate defines followed by an immediate value. In order to evaluate a value, it must be of the form E[T] where E is an evaluation context and T is a rule trigger. Now by definition, E is of the form D[C[]], where C is a control context and D is a definition context containing all the defines at the beginning of V, followed by a hole. So C[T] is the immediate value following the definitions in V. We now consider the posibble forms of C[]: C[] is a []: That is, T itself is the immediate value at the end of V. But inspecting the rule triggers reveals that no trigger is an immediate value, so this cannot occur. C[] is of the form: (if * *). Combinations are not immediate values. So, since C[] is an immediate value, it cannot be a combination. C[] is of the form: (set! var ). Again, this is not an immediate value. So we conclude that V cannot be of the form E[T], and therefore no evaluation rewriting step applies to V. Handout 14 Problem 6: ::= ..... | **) | .... Handout 15 Problem 1a: Printable Value detector: We define a tester for whether a printable value equals an arbitrary value: (define (pv-equal? pv1 value) (cond ((null? pv1) (null? value)) ((boolean? pv1) (and (boolean? value) (if pv1 value (not value)))) ((symbol? pv1) (and (symbol? value) (eq? pv1 value))) ((integer? pv1) (and (integer? value) (= pv1 value))) ((pair? pv1) (and (pair? value) (pv-equal? (car pv1) (car value)) (pv-equal? (cdr pv1) (cdr value)))) (else (error "not-printable" pv1)) Let be some printable value. Then the desired V0-detector is: (define (detectv0 value) (pv-equal? value)) Handout 15 Problem 2: Part A: Here we need any expression, , with the property that (**) ev-val( ( 'S) ) = ev-val( '(S 'S) ) Scheme->C -- 15mar93jfb -- Copyright 1989-1993 Digital Equipment Corporation > (pp (((lambda () (define (make-self-apply qs) (list qs (list 'quote qs))) make-self-apply)) (quote ((lambda() (define ((make-self-apply qs) (list qs (list 'quote qs))) make-self-apply))))) (((lambda () (define (make-self-apply qs) (list qs (list 'quote qs))) make-self-apply)) (quote ((lambda () (define (make-self-apply qs) (list qs (list 'quote qs))) make-self-apply)))) PART B Another version of satisfying (**) obtained by "in-lining" the definition of make-self-apply in the version of Part A is (lambda (qs) (list qs (list 'quote qs))) yielding: > (pp ((lambda (qs) (list qs (list 'quote qs))) '(lambda (qs) (list qs (list 'quote qs))))) ((lambda (qs) (list qs (list 'quote qs))) '(lambda (qs) (list qs (list 'quote qs)))) We can also take the version of Part A and replace the first "list" by nested cons's (lambda () (define (make-self-apply qs) (cons qs (cons (list 'quote qs)) '())) make-self-apply) yielding: > (pp ((lambda () (define (make-self-apply qs) (cons qs (cons (list 'quote qs)) '())) make-self-apply)) ((lambda () (define (make-self-apply qs) (cons qs (cons (list 'quote qs)) '())) make-self-apply))) PART C The idea this time is to define so that (***) ev-val( ( 'S) ) = ev-val( '((S 'S) (S 'S) ) Then ( ') will be the required doubly self-reproducing expression. (define ( s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list 'quote a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs))) ;Value: (define R ( (quote ))) ;Value: r (pp r) (( (quote )) ( (quote ))) ;Unspecified return value To get a completely self-contained doubly self-reproducer we apply the value of (lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list 'quote a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs))) to the quote of itself: (define r ((lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list 'quote a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs))) (quote (lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list 'quote a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs)))))) ;Value: r (pp r) (((lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list (quote quote) a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs))) (quote (lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list (quote quote) a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs))))) ((lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list (quote quote) a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs))) (quote (lambda (s) (define (make-apply a b) (list a b)) (define (make-quoted a) (list (quote quote) a)) (let ((s-of-qs (make-apply s (make-quoted s)))) (make-apply s-of-qs s-of-qs)))))) ;Unspecified return value Handout 15 Problem 3: Suppose SS were half decidable, and let H be a half-decider for SS. Since SS is non-trivial, there must be an S-expression, X, which is not in SS. Define to be: (lambda (qs) (if ( (make-apply 'H (make-self-apply qs))) X X)) where is a half-decider for Halts. Now for any Scheme expression, S: If (H '(S 'S)) halts, then by definition, ( 'S) -*-> X. Since X is not in SS, by evaluation invariance ( 'S) is not in SS. Since H is a half-decider for SS, this implies that (H '( 'S)) does not halt. Conversely, if (H '(S 'S)) does NOT halt, then by definition, ( 'S) does not halt either. Since SS contains all of the non-halting scheme expressions, we conclude that ( 'S) is in SS, and again, since H is an SS half-decider, it follows that (H '( 'S)) DOES halt. So for all S, (H '( S 'S )) halts iff (H '( 'S)) does not halt. Now let S be and we obtain an immediate contradiction. Handout 15, Problem 4a: Let F1 be (list 'a1 'a2 'a3..... 'a_n) where a1, a2, ... , a_n are the S-expressions that are in script_F_1, and let F2 be a similar list for script_F_2. Then a half-decider for script_S_2 is (lambda (qs) (or (member qs F2) (if (member qs F1) (spin) (half-decide-script_S_1 qs)))) 4b: If we have a separator that fails to halt for only a finite number of cases, then we can obtain a real separator by patching this separator with a lookup-table of answers for the expressions that it gets wrong. But by Scott's Rice's theorem, there can be no such separator. Thus the number of input expressions for which the separator fails must be infinite.