Lambda the Ultimate

Thanks for the pointer!

One issues I have with Djinn is it giving you the implementation from scratch, not reusing existing functions.

I mean, instead of getting f x = x I would prefer getting f = id.

Also, ignoring libraries means it knows nothing about lists or orderings, so my type from the original post cannot be solved.

You can teach Djinn about Ordering. And let's use Maybe instead of lists just to see what happens. Oh, and the context will have to be replaced by a function.

Djinn> data Ordering = LT | EQ | GT
Djinn> h ? (t->t->Ordering) -> Maybe (t,a) -> Maybe (t,b) -> Maybe (t, Either a b)
h :: (t -> t -> Ordering) -> Maybe (t, a) -> Maybe (t, b) -> Maybe (t, Either a b)
h a b c =
    case b of
    Nothing -> Nothing
    Just (d, e) -> case a d d of
                   LT -> Nothing
                   EQ -> Nothing
                   GT -> case c of
                         Nothing -> Just (d, Left e)
                         Just (f, g) -> Just (f, Right g)

Hmmm, doesn't really look anything like what you had in mind, does it? :)


((a -> a) -> (b -> b)) -> ((a -> Maybe a) -> (b -> Maybe b))
Is a function that takes 3 arguments, the last of type b, and returns a Maybe b. But we already have return :: b -> Maybe b. So the solution is simply const (const return) which ignores its first two arguments.

So I'd suggest the first step, before using any theorem prover, is to erase extra parentheses by hand so it's easier to parse by eye.

Well, I mentioned that Nothing is bad solution, but I should have added that Just wrapping the third argument is not good as well.
I would like to use all arguments.

That's why the solution with all arguments used is listed first. :)

Well, but it is still not what I intended.
For one, it can never return Nothing.

I have a solution in mind, which would work in impure language (requires at least exceptions). So I guess what I need is to CPS-transform some of the function types involved, and then see if Djinn can find what I meant.

BTW, the intent of the function was given a container update function (which is similar to map, but is not as natural) and a possibly failing element transformation to obtain a possibly failing container transformation.

It might not be what you have in mind, but it never returns Nothing.
There's a Just constructor on the outside.

Yes, the only way to get Nothing is constant Nothing variant.

I changed the type to ((a -> c) -> (b -> d)) -> ((a -> Maybe c) -> (b -> Maybe d)) so there are less possibilities to cheat, and the only inhabitant found is constant Nothing.

The problem (or feature) is lack of speculative execution: the code must early commit to one of the choices - either to return Nothing or to call container update (and risk that element update fails, at which point it is too late to return Nothing). The tantalizing part of this is that impure implementation is obvious.

Occasionally, as a mathematician, I want to prove result A using result B even though I already have another proof not using B. I guess that's exactly what you're asking for. Thinking purely in terms of logic I'm not 100% sure it's a well-defined notion but thinking computationally we have a pretty good idea of what it means for a function to depend on an argument. So your question gives a way to make rigorous sense of the notion of a proof that must depend on a premise. Interesting.

It's a perfectly well-defined notion in logic -- it's a relevant logic. In a relevant logic, a premise in a proof must be used in the derivation. (Hence the name -- the premises must be relevant.) This amounts to rejecting the axiom of weakening -- i.e., rejecting the axiom that A -> (B -> A).

If you also drop the principle of contraction, then you get linear logic.

A mathematician, speaking informally, is happy to say that one proof depends on another when using classical logic and when their proofs are full of weakening steps. Similarly, the original question doesn't ban us from using weakening in general, just certain specific uses of it. Is it straightforward to define a logic that keeps weakening in general, but makes sense of the idea of using certain specific premise? For example could we use a slightly restricted axiom schema of weakening and get meaningful results? Just banning the use of weakening for the required premises themselves wouldn't do, for example in the classical case banning p->(Q->p) for a specific Q would still leave us free to use p->(~~Q->p) which is essentially the same thing.

Yes, it makes sense. Look at the ? and ! connectives in linear logic.
You just need to mark the things that can be weakened (or not weakened).

Yes, this makes sense. It's pretty easy to cook up a logic that does the job. I'll use natural deduction because hey, that's what I know best.

The basic idea is that the usual presentation of logic looks more or less like this:

A,B ::= P | A -> B
Gamma ::= nil | Gamma, A true

P are the atomic formulas, and we'll only look at implication as our only connective. A derivation Gamma |- A true is a proof that the formula A is true in some context of hypotheses, denoted by Gamma. In natural deduction style, we have a hypothesis rule and an intro and elim rule for implication:

Gamma |- B true
----------------------- (weak)
Gamma, A true |- B true


Gamma, A true, A true |- B true 
------------------------------- (contract)
Gamma, A true |- B true


-----------------------  (hyp)
A true |- A true


Gamma, A true |- B true
----------------------- (-> Intro)
Gamma |- A -> B true


Gamma |- A -> B true   Gamma |- A true
-------------------------------------- (-> Elim)
Gamma |- B true

Relevant logic changes this by throwing out the weakening rule. So what happens if we want to allow some hypotheses to use weakening, and some that don't? Well, the easy thing to do is just to add a new context of strictly used hypotheses! Then we can change our judgement from Gamma |- A true to Gamma; Delta |- A true. This means that A is true, under the assumptions in Gamma, and the assumptions in Delta, and furthermore every assumption in Delta is actually used at least once.

A, B ::= P | A -> B
Gamma ::= nil | Gamma, A true
Delta ::= nil | Delta, A strict

-----------------------  (Strict hyp)
nil; A strict |- A true


--------------------- (Unrestricted hyp)
A true; nil |- A true


Gamma; Delta |- B true
------------------------------  (weak)
Gamma, A true; Delta |- B true


Gamma, A true, A true; Delta |- B true
-------------------------------------- (contract)
Gamma, A true; Delta |- B true


Gamma; Delta, A strict, A strict |- B true
------------------------------------------  (strict contract)
Gamma; Delta, A strict |- B true


Gamma, A true; Delta |- B true
------------------------------ (-> Intro)
Gamma; Delta |- A -> B true


Gamma; Delta |- A true   Gamma; Delta' |- A -> B true
----------------------------------------------------- (-> Elim)
Gamma; Delta, Delta' |- B true


Gamma; Delta |- A true    Gamma; Delta', A |- B true
---------------------------------------------------- (strict cut)
Gamma; Delta, Delta' |- B true

The key idea that makes this work is that the rules with multiple premises divide the strict hypotheses between them, so that you know that each branch of the proof guarantees using some of the strict hypotheses. (You can use contraction to replicate a hypothesis, if both branches turn out to need it.)

If you internalized the notion of relevance into intuitionistic logic as a new modality, I think that it would turn out to be box. (Maybe even S4's box?) Then you could give it a categorical semantics as a comonad over a CCC. But I'm pretty shaky on semantics in general, and categorical semantics of modal logic is starting to get out of my depth. So take this last paragraph with a grain of salt.

...is a theorem prover for your logic...

So these questions can certainly be answered by Djinn:

Djinn> :set +m
Djinn> f ? ((a -> a) -> (b -> b)) -> ((a -> Maybe a) -> (b -> Maybe b))
f :: ((a -> a) -> b -> b) -> (a -> Maybe a) -> b -> Maybe b
f a b c =
    Just (a (\ d ->
             case b d of
             Nothing -> d
             Just e -> e) c)
-- or
f a _ b = Just (a (\ c -> c) b)
-- or
f _ _ a = Just a
-- or
f _ _ _ = Nothing

Djinn> g ? (a -> (a -> r) -> r) -> (a -> a)
g :: (a -> (a -> r) -> r) -> a -> a
g _ a = a

Even though Djinn does not necessarily give you all possible implementations the fact that you only get one answer for the second query is a good hint that it's the only one.

Djinn has simple heuristic so that it tries to use as many variables as possible to avoid trivial solutions. So the implementation of f is one that might do what you want.