axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] McCarthy on dataspaces


From: Robert Harper
Subject: Re: [Axiom-developer] McCarthy on dataspaces
Date: Sat, 15 Sep 2018 10:19:43 -0400

it's called intuitionistic type theory

On Sat, Sep 15, 2018 at 04:47 Tim Daly <address@hidden> wrote:
In the video "The Most Beautiful Program Ever Written"

Byrd derives

(define eval-expr (lambda (expr env)
  (pmatch expr
    [,x (guard (symbol? x)) (env x)]
    [(lambda (,x) ,body)
      (lambda (arg)
        (eval-expr body (lambda (y) (if (eq? x y) arg (env y))))))]
    [(,rator) (,rand)
      ((eval-expr rator env)
       (eval-expr rand env))])))

He points out that it has lexical scope and higher-order functions.

At  a glance it is obvious that the program is the lambda calculus
 x | 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 captures
local scope, aka data, in a lambda binding. Since it is recursive the
environment is built and scoped as closures in the 'env' argument.

It seems straightforward to add types (as lambda expressions, not
as the traditional symbol form like alpha, etc.). Depending on how
they 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 these
elementary procedures may be, and how more complex procedures are
constructed 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 a
computable function to guide us, and computability relative to a given
collection of initial functions is easy to define.

Procedures operate on members of certain data spaces and produce
members of other data spaces, using in general still other data spaces
as intermediates. A number of operations are known for constructing
new data spaces from simpler ones, but there is as yet no general
theory of representable data spaces comparable to the theory of
computable functions."

Most of the treatments I've seen fall back upon set theory to handle
Gamma, such as saying that items to the left of a turnstile are sets
or 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 book

Are you aware of any references that focus on a "theory of representable
data spaces" that does not involve sets?


Tim





--
(c) Robert Harper. All rights reserved.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]