Sequent was coming along sortof nicely, but I am reminded of the enamoring simplicity of Lisp. It was the first functional language (right?), because it could be implemented before anybody knew how to program functionally. That is also the source of some of its warts, but all in all it was a great start. My question: is there a simple meta-circular definition of a knowledge-oriented language like the one I am trying to build? Maybe if I can find something small and essential, it will allow me to explore the programming space with it without getting lost in implementation details.
I think tactics may be the key. I have always thought of tactics as a layer above the core proof engine (which is good for verifiability), but maybe an essential kernel takes tactics more seriously, and the core logic less seriously.
Here is a potential guiding principle: you have knowledge, and with tactics you manipulate it. The first place my mind goes is to higher-order tactics, essentially interacting with knowledge through Lisp. Obviously my mind would go there, being a functional programmer. But I am currently looking for an essential meta-circularity, so it seems reasonable that tactics would be represented as knowledge as well, and then the language allows you to use a piece of knowledge you have as a tactic.
What is the information in a tactic? This could be the necessary first modeling task of the language. In general a tactic looks at the context and the environment (those are probably the same thing) to make its decision about how to manipulate it. For example, we can imagine a tactic known which looks at the current goal and finds a matching hypotheses to eliminate it. That is one of the simplest (but nontrivial) tactics. In Sequent's language, what is the answer to "what does it do?"
known : (H A B ['A |- 'B] -> ['A 'H |- 'B 'H])
Yes, that seems like a good plan: reify the whole environment into an object of the language. Of course, such a thing should be provable, which means that we have to have enough apparatus to prove this (i.e. we need to be able to refer to things like A and B: "the rest of the stuff"). We also need enough apparatus to use this statement as a tactic, the proof does not play into it (that's good?). There is some pattern matching going on here, presumably; however it is possible that it is captured by some in-language definition of |-.
(To think in this (half-)language, it seems that I need to further separate myself from "doing", moreso even than required by purely functional programming.)
The tactic layer is much like the macro layer in Lisp -- you can only use it while developing (compiling), and later you generate (run) a program. It could be seen as putting the user inside the compiler -- that's exactly what I want. It should quote the elements of the program so they can be manipulated as objects.
Of course, then the language must be good at manipulating objects (which it is not really designed for). Can we instead view the objects as knowledge -- quoting predicates into metapredicates? There is this cumbersome approach:
P: A -> B
-- becomes
P ['P has type 'X]
X ['X is 'A -> 'B]
A ['A is variable named "A"]
B ['B is variable named "B"]
Which, if it gives us headway, could be okay, just don't ever make me look at it. We could always introduce a functional syntax like Oz did, reducing to logical statements underneath. Then perhaps we could write known like a Prolog program:
known: (
A B ['A |- 'B]
x xT y yT
[view 'A as 'x : 'xT + 'A1]
[view 'B as 'y : 'yT + 'B1]
->
['A1 |- 'B1]
)
Who instantiates those variables though? It is not much use if the user has to instantiate them. Also, how is known proved?
I am tempted to introduce a dependently typed calculus so that we know what can be proved (the terms of the language are proofs), but I worry that it would contaminate the purity of thought of the language, as functional programmers would find it easiest to program functionally instead of logically. However, considering the motivation: CHI and functional programming, we would only be exposing the underlying apparatus. In the name of metacircularity, the underlying apparatus ought to be the same as the system, in some sense.
If I give in to this temptation, I am looking for a dependently typed calculus (system IG maybe ;-) and a library for reflecting terms. Could a library of reasonable minimality handle meta-theorems like known? I suppose if we encoded the calculus in the language itself (hmm, metacircular) then meta-theorems would have the same provability status as normal theorems without that calculus. The abstract picture is getting clearer.
If I am to write Sequent's calculus in Sequent, I know I am going to have to do better than brute-forcing variables. Names are the key, and manipulating names should be painless and obvious. Fortunately, we have the liberty of being able to design a language specifically for manipulating names; unfortunately, we have the responsibility of designing a language for manipulating names. The library should reflect terms in a name-respectful way -- allowing meta-programs to access the textual content of the names (because that can be important), but also only allowing them to be manipulated in some reasonable ways: for example, you should not be able to remove a name from its binder (though you can call a different variable by the same textual name). So names are first-class in some way, they are not determined by their textual representation.
We would like our name library to handle:
- Preventing variables escaping from their binders
- Preventing free variable capture
- Safe substitution
- Alpha-equivalence
(By the way, can I just say how great it is not to be worrying about consistency!)
Free variable capture, in the lambda calculus, happens in a situation like this:
(\x y. x) y -> \y. y
Either the original term is offensive in some way, or the reduction was done incorrectly. I feel like the first option is a better way to think. Basically I'm thinking of bound variables as "covariant" -- i.e. to construct a lambda, you do not give it a variable and a body, it gives you a variable and you give it back a body. It's the classic HOAS representation:
lambda :: (Expr -> Expr) -> Expr
Introspection can be done by passing to the body-function a dummy variable. But then you have to know how to make a dummy variable.
If we express syntax trees as relations as above, then how do variables play this role? Eg. encoding this lambda:
t = \x. x x
-- becomes
(x ['x variable] ->
['t is lambda 'x 'b]
['b is 'x applied to 'x])
I don't think that is right. Maybe we get rid of lambda and define in terms of application:
(x ['x term] h ['h is 't applied to 'x] ->
['h is 'x applied to 'x])
Yes I think that defines t. Does it do so in a way that a program could make decisions based on the structure of it? For example, what happens in an abstract situation like known? I suppose known does not introspect the terms itself, but is given the "knowledge" of an introspection done by the kernel. So a definition of known can give its action in terms of bare knowledge, just like the above second definition of known. The trick is (still) automating it, and not having to fill in all the witnesses of the tactic yourself.
Perhaps the problem is that we are not encoding feedback. This system works well for the mathematician who is essentially writing down his process and being followed by a computer. But we need a way to ask the computer to try something and tell us what happened, and that kind of sentence may not occur naturally as a proposition. As in Coq, maybe those instructions are more naturally terms, diving truly deep back into the functional world.
Tactic = Context -> Context
or something like that. I am again afraid (going in circles here) of contaminating the system with functional ideas.
I think we must have some idea of evaluation of the terms we have constructed by their types. But perhaps tactics can be specified not as some formal symbol game, but more like my engineer-picture would:
known : (
A B ['A |- 'B]
->
D ['A |- 'D]
(h ['h in 'B] ['h not in 'A] -> ['h in 'D])
(h ['h in 'B] ['h in 'A] -> ['h not in 'D])
)
That is, we return a sequent whose actual content is unknown, but we know things about it. Of course, the implementation of this will not be as easily guided as the earlier formulations (though perhaps we could use the earlier formulations to construct this one...).
Oh look, these are backwards from sequents. They are cosequents. If [_ :- _] is a proper sequent, then a cosequent is:
A B
(P (['A :- 'B] -> P) <-> ['A |- 'B]
Since we are getting on to computing within the environment, I would still like this to be an organizational system for code in real languages (so that I get libraries for free!). So I picture different kinds of arrows:
X -> Y -- a Sequent arrow, the weakest kind probably
X //> Y -- a Javascript arrow (or something)
You can manipulate Javascript arrows and generate code from them, but you can't execute them in the environment (unless your environment is written in Javascript). You can execute Sequent arrows within any Sequent environment. And by structural induction (i.e. sufficient hypotheses about ->), you could prove:
X Y ((X -> Y) -> (X ~> Y))
Thus converting a Sequent method to a Javascript method.
This indicates perhaps a way to get started on the essential core: encoding the rules for ->. In terms of what? In terms of ->, of course.
Oh, a quick note on syntax. Since we are going all meta, it would be nice to have arbitrary syntax to refer to propositions and expressions, so that we can express Javascript arrows in familiar syntax, even though there is probably a level of quotation involved. But syntax is not to be reasoned about, just viewed, so the word order and stuff in bracket propositions isn't really important, that's just the way of displaying an intensionally defined proposition.