[Phil-logic] FOL Carefully Defined - Frugally Assisting Purely-Functional Operation
Dennis E. Hamilton
dennis.hamilton at acm.org
Sun Dec 19 21:01:03 CET 2010
Roger,
Although we here wandered hand-in-hand into the weeds of computation
theories, your comment about pure functional programming rang true for me in
terms of pure applicative programming too.
For early work, starting out with a purely-functional/-applicative core, I
require a front-end assistant. These assistants are known as processors for
the Frugal language family, which allows some of the nasty bits that are
needed for human usability at any level to be provided in front of the core
engine (B, Below).
There is also an interesting foundational/theoretical matter with regard to
the interpretation of computer codes that comes up in this approach (A,
Below).
- Dennis
A. SOME FOUNDATIONAL FEATURES OF COMPUTATION
My particular little computer formulation has what I seem to have always
regarded as the fundamental linguistical-attention capability of computers
(and I thank Michael Polanyi for some distinctions in this regard concerning
"attention").
How this shows up these days has to do with the fact that computer models,
at least the fundamental ones, are essentially one-sorted, where any object
of discourse can be a procedure and any object of discourse can be the
operand of a procedure. [To stick with FOL, functions are not in the object
of discourse, there is only data which can be construed either way as
procedure code or data code depending on where it figures in the context of
an applicative operation.]
This is enough, I believe, to sharpen the notion of the difference between
computation and computational procedures and the logical representation of
functions. In computation, we don't infer results, we inspect for them, and
identity is a deterministic primitive. So in the simplest form of PA as a
logical theory, one does not need to do more than distinguish the origin (my
preference being 0 rather than 1) and have a successor function. One can
establish further operations by definitions that establish what inferences
can be made concerning a successfully-represented function.
For example, (x)[x=0 -> dim(x)=0] and (x)(y)[x=y' -> dim(y) = x] represents
the diminish function.
For a computational system to be computationally complete (in that all
computable functions on the single sort are representable by algorithmic
procedures of the system), that is not good enough. Continuing with the
case of the domain of PA, to be able to determine that x is a predecessor of
y, I need at least an identity primitive and I need a way to find the
predecessor of a given value. I can assume it because it is representable
(in FOL), and if the system is computationally complete, there is a way to
express it. In fact, there need to be in the computational system at least
a deterministic computational interpretation of "=" (and its negative) and
there actually needs to be an operation for dim(x), not just successor(x).
[To oversimplify, for every constructor there must be a suitable selection
of destructors (accessors).]
In short, I have to wire in more than successor and "=" to get to what in a
logic is accomplished by representing functions through introduction of
predicates and demonstration of the correspondence. Basically, I need a
(preferably-)closed system in which there are primitive operations by which
any object can be transformed to any other by a finite sequence of
successive applications. Then we can talk about how one can build up
representations of all computable functions from such primitives and a
complete applicative system over them.
Then, having teased all of that out, one next needs to deal with the fact
that type and distinguishing objects by markers or even predicates is not
intrinsic but figures critically in being able to manifest the
representation of richer entities, establish their representation's
computational completeness (to the degree that is achievable), and having a
computational logic that distinguishes among them and supports reasoning
about them.
The foundational importance of type, here, has to do with the fact that
having predicates that assert type is not necessarily a partitioning of the
underlying (semantic) objects of discourse for a computational system, and
distinguishing satisfaction of certain predicates leaves us with some odd
decision problems. I don't know whether we are thereby forced to tag things
in the computational representation or not. How far, and no farther, one
can get without tagging (e.g., reflection in contemporary programming-system
parlance) is a question I want to explore as part of this undertaking.
There are some computability pratfalls to understand.
B. THE FRUGAL-ASSISTANT GAME
The purely functional/applicative, core mechanism that I have in mind is so
pure that it doesn't even have symbols for free variables in any
conventional sense. This is not a technical problem, but it is certainly a
problem for humans. The only constants in procedure code that qualify as
variable references in any programming-system sense are the one called
ob_self and another called ob_arg. That's it until I decide whether I need
to extend that tiny set to expedite tail recursion (and perhaps handling of
purely-functional continuations as another significant speed-up).
The purely-functional evaluator, which is well-defined enough that I could
build one (after correcting some bugs in a sketch I created), is called
oMiser and it is only good for thought experiments unless there is a way to
operate with it that is humanly manageable.
That is where Frugal comes in. Frugal processors are front-end fixtures
that do the nasty part of holding onto code by names, allowing substitution
of the named code into other code being built, and providing for iterative
use of the oMiser evaluator. Frugal provides the counterpart of a
read-eval-print cycle in a front end to the purely functional mechanism of
interest. It accepts an applicative language that allows assembly of oMiser
codes without the ultimate pain of purely-applicative expression and
construction.
I always thought of this as being akin to the model that the CDC 6600 family
of computers demonstrated where the computational engine was a
fire-breathing computational processor and that was all it could do, with
all of the construction of programs, accomplishment of input-output, etc.,
relegated to peripheral processors that provided those functions off-line to
the primary computer. (Univac Larc had a similar structure but the
computational processors shared a single input-output processor and they
could off-load work onto it via shared memory as I recall.)
I was starting to think of Frugal as a browser, but I realize, thanks to
your note, that I should call it an assistant. (It is an user agent, in the
sense now used with regard to the Internet, but one on my desktop PC or
smartphone phone or whatever would clearly be serving as an assistant.)
I need something like that to test oMiser implementations. Frugal accepts a
scripting language that translates to oMiser structures (usable as procedure
and/or data including both of course), but that is far handier, allows
storage of the structures in a persistent form, pretty-prints them, etc.
This is meant to be part of a bootstrapping/iteration process by which I can
explore how to keep the pure around while also dealing with the more
interesting situations of distributed stateful and interactive processes (or
establish that oMiser is not enough of a launch pad for that, a valuable but
not so exciting result). One obvious benchmark would be getting to a point
where some [n]Miser is sufficient for implementing [n]Frugal without leaving
the box, as it were. (Umm, I have said too much already as far as the
interests on this list go, but I believe the handling of extensibility in
the system is also critical and shows up fairly early, concurrent with
reconciliation of the issue concerning distinguishable types.)
-----Original Message-----
From: phil-logic-bounces at philo.at [mailto:phil-logic-bounces at philo.at] On
Behalf Of Roger Bishop Jones
Sent: Saturday, December 18, 2010 14:58
To: phil-logic at philo.at
Subject: Re: [Phil-logic] FOL Carefully Defined
[ ... ] We did briefly consider
using his Miranda language as the metalanguage for
ProofPower, but we discussed the problems involved
in doing an LCF proof tool in a pure functional programming
language (with David Turner), and he conceded that he didn't
know how it could be done.
[ ... ]
So what are these foundational concerns which make you
interested in FOL at present?
Roger Jones
_______________________________________________
Phil-logic mailing list
Phil-logic at philo.at
http://philo.at/cgi-bin/mailman/listinfo/phil-logic
More information about the Phil-logic
mailing list