
From:  Robert Harper 
Subject:  Re: [Axiomdeveloper] McCarthy on dataspaces 
Date:  Sat, 15 Sep 2018 10:19:43 0400 
In the video "The Most Beautiful Program Ever Written"Byrd derives(define evalexpr (lambda (expr env)(pmatch expr[,x (guard (symbol? x)) (env x)][(lambda (,x) ,body)(lambda (arg)(evalexpr body (lambda (y) (if (eq? x y) arg (env y))))))][(,rator) (,rand)((evalexpr rator env)(evalexpr rand env))])))He points out that it has lexical scope and higherorder functions.At a glance it is obvious that the program is the lambda calculusx  lambda x  (e1 e2)but it also has an interesting wrinkle in the environment encoding(aka Gamma) in that the 'env' argument is an _expression_ that captureslocal scope, aka data, in a lambda binding. Since it is recursive theenvironment is built and scoped as closures in the 'env' argument.It seems straightforward to add types (as lambda expressions, notas the traditional symbol form like alpha, etc.). Depending on howthey get handled in closures they could be static or dynamic.But McCarthy raises an issue of data.From McCarthy "Towards a Mathematical Science of Computation""Procedures are usually built up from elementary procedures. What theseelementary procedures may be, and how more complex procedures areconstructed from them, is one of the first topics in computer science.This subject is not hard to understand since there is a precise notion of acomputable function to guide us, and computability relative to a givencollection of initial functions is easy to define.
Procedures operate on members of certain data spaces and producemembers of other data spaces, using in general still other data spacesas intermediates. A number of operations are known for constructingnew data spaces from simpler ones, but there is as yet no generaltheory of representable data spaces comparable to the theory ofcomputable functions."Most of the treatments I've seen fall back upon set theory to handleGamma, such as saying that items to the left of a turnstile are setsor that imperative program actions modify a set of known variables.The closest I've seen to a theory of "representable data spaces"occurs in the Let Over Lambda bookAre you aware of any references that focus on a "theory of representabledata spaces" that does not involve sets?Tim
[Prev in Thread]  Current Thread  [Next in Thread] 