[racket] proof assistants, DrRacket and Bootstrap

Easy. 

;; SchemeExpression is one of: 
;; --- 

;; SchemeValue is one of: 
;; --- 

;; Environment = [Listof [List Variable SchemeValue]]
(define base-environment 
  `((sin ,sin)
    (cos ,cos)
    (richter ,(lambda (x) (cons x '(bill))))
    ...))

;; SchemeExpression -> SchemeValue
(define (evaluate e)
  (evaluate-in-context e base-environment)) ;; <--- This is '() in HtDP 

;; SchemeExpression Environment -> SchemeValue 
(define (evaluate-in-context e)
  (cond 
    [(constant? e) ...]
    ...))





On Oct 15, 2014, at 9:06 PM, Bill Richter wrote:

> Matthias, I'm still thrilled with your advice about writing a ML interpreter in ML, but I think what you told me doesn't suffice, and in particular:
> 
> MF> 1. HtDP explains the above in a couple of sections. 
> 
> I think HtDP only does part of the job.  I think there is nothing about Scheme evaluators past Section 17.7, where you extend the 14.4 evaluator to functions:
> HtDP> The goal of this section is to extend the evaluator of section
> HtDP> 14.4 so that it can cope with function applications and function
> HtDP> definitions.
> In the Section 14.4 evaluator you don't even have variables:
> http://htdp.org/2003-09-26/Book/curriculum-Z-H-19.html#node_sec_14.4
> I'm sure HtDP is fine for a first course, and I profited from reading it again, but I think a better job is done in the OCaml manual, in Sec 1.7 of 
> http://caml.inria.fr/pub/docs/manual-ocaml/coreexamples.html
> where they have something a lot like your 
> 
> MF>   type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast 
> MF>   type val = BASIC of int | FUNCTION of val -> val | ...
> 
> But what I don't like is the OCaml manual's 
> 
> Om> We first define a function to evaluate an expression given an
> Om> environment that maps variable names to their values. For
> Om> simplicity, the environment is represented as an association list.
> 
> That's fine, as long as the Scheme/ML program we're evaluating is self contained, because the only variables will be the ones we define in our program.  But what if the program has free variables which are already defined?  How do we get our trees to use the values in a Scheme environment already defined?  I am sure you racketeers know the answer, and maybe it would be a good exercise to put in your second edition:
> http://www.ccs.neu.edu/home/matthias/HtDP2e/
> All I can guess is that is Sec 17.7, you say that a 
> HtDP> the function's name [and] the parameter name [are] symbols
> so probably all variables are represented in the tree as symbols, and I guess we need a function that will take these symbols and return their values given in the bigger environment.  
> 
> -- 
> Best,
> Bill 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4463 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20141015/cbd45d72/attachment.p7s>