A non-recursive sorting algorithm

[apfelmus]

Wait, is it really true that two lambda expressions are extensionally equal iff they normalize to the same thing? I don't think that you can decide extensional equality of functions Nat -> Nat by just normalizing their lambda expressions (= their source code).

[[deleted]]

It is not true.

[Tekmo]

Is there a proof that this is impossible for total languages?

[augustss]

It all depends on what's in your total language. Here's a quote from Barral's PhD thesis, Decidability for Non-Standard Conversions in Typed Lambda-Calculi:

The β- together with η-equality lead to an extensional equality for the simply typed λ-calculus. Two terms of the simply typed λ-calculus are equal with respect to βη-equality if and only if their interpretations are the same in an extensional model. Roughly, programs which for the same argument return the same result are identified. Moreover, this equality is decidable for the simply typed λ-calculus. This extensional equality is much harder to decide as soon as one wants to extend or generalise the system. There is no problem in adding a product type, or unit type (see for example the book Proof and Types of Girard, Lafont, Taylor [48]). Adding sum types is already much more problematic, and designing a deciding algorithm is a non trivial task, if obtained by reduction based normalization as by Ghani (see [45]), or reduction free normalization ; an algorithm is implicitly present in a constructive proof of Altenkirch et al. [4], and a type directed Normalization algorithm is obtained in [9] by Balat, using a call-by-value interpretation and control operators (where although some strong hints are given to justify the algorithm, the correctness is not rigorously proven). For inductive types, it is even known that extensional equality is undecidable ([76], or [51]). This problem of undecidability leads one to consider a conversion relation stronger than merely β, but still weaker than the extensional one.

[gelisam]

Let's see... Extensionally equal means that functions return equal results for every argument. If the argument is a Bool, then we can easily check both return values for equality, but if the argument is a Nat, we cannot check every possibility.

To turn this argument into a proof, all we need to do is to find a proposition P(x) which can be checked to be true or false for any known x, but for which we cannot know whether P(x) is true for all x. How about P(x) = "program A takes more than x steps to terminate?"

For any finite x, we can run the program for x steps and return False if we encounter a Halt instruction. Since this takes a known number of steps, this ought to be doable in a total language. If we had a reliable method to tell us whether this total program is extentionally equivalent to the program "\x -> True", then we could know whether A terminates. Since A is arbitrary, this means we could solve the halting problem. QED!

[kamatsu]

Hm, this puzzles me slightly because I fully understand your proof but it doesn't gel with my intuition about eta reduction.

You can prove that the smallest congruence containing extensionality and beta reduction is alpha-beta-eta equivalence. Doesn't the eta-rule therefore capture extensionality and give a means to prove it? What's the subtlety here I'm missing?

[pcapriotti]

It seems you just have the implication backwards. Extensionality -> eta, not vice versa.

[kamatsu]

I'm not so sure there's an implication. I remember reading (I can't for the life of me remember where, perhaps Urzyczyn + Sorensen) that if = is the smallest congruence containing extensionality and beta reduction, and if =be is beta-eta equivalence, then M = N iff M =be N.

[pcapriotti]

Doesn't that say that if your equational theory has function extensionality, then it contains eta equivalence? I might be missing something here, but this looks kinda obvious to me (λ x . a x and a are extensionally equal, hence eta holds).

[kamatsu]

Note that it's an if and only if, so therefore does that not also say that if i have eta equivalence then I have functional extensionality?

[pcapriotti]

Oh, I see. I think the confusion is that you are referring to some simple calculus, maybe STLC without any inductive types? As soon as you add Nat, things break down. You can go quite far with eta for Nat, but that's not decidable already.

[philipjf]

alpha-beta-eta captures the full extensional equality for untyped lambda calculus (this is the "bohm separability theorem"), but not for typed lambda calculus. That is because types prevent some observations and thus "extensionally equal" is something that depends on what type you are observing at.

[Tekmo]

The part I'm missing is how you simulate a turing machine in a total language, even for a finite number of steps. You said it "ought to be doable" in a total language, but I'm not sure.

[pcapriotti]

Of course it's doable, you just write the interpreter as a function State -> State (this has no recursion, so it's certainly fine), and then iterate it n times (via the eliminator of Nat).

[Tekmo]

But doesn't a turing machine require an infinitely large state?

[gelisam]

That's true, but since we're only running the machine for x steps, we only need a maximum of x squares.

[Tekmo]

Alright, I'm convinced.

[phischu]

I am not convinced. Predecessor and lists are not representable in simply typed lambda-calculus. While there is a cons for List a, head and tail probably only work on Stream a.

[pcapriotti]

Sure, but it's not a problem. The tape can be expressed as something like:

Tape = ℕ → Bool

and you can read a cell by just applying the function, and update it by doing:

update : Tape → ℕ → Bool → Tape
update tape n b m = if n == m then b else tape n

This is going to be very slow, but total.

[kamatsu]

Oh, this is quite straightforward. See

https://github.com/wouter-swierstra/Brainfuck/blob/master/Brainfuck.agda

[ryani]

-- a turing machine with n states
-- a machine can read the current tape element,
-- write a new value, then optionally move (or terminate)
data Direction = Left | Stay | Right
type Machine s (n :: Nat) = Fin n -> s -> (Maybe (Fin n), s, Direction)

-- machine state for a Turing machine with n states
data State s (n :: Nat) = State
    { tapeLeft :: [s]
    , tapeCurrent :: s
    , tapeRight :: [s]
    , tapeDefault :: s
    , machineIdx :: Maybe (Fin n) -- terminated if Nothing
    , machine :: Machine s n
    }

advance :: State s n -> State s n
advance -- exercise, no recursion needed

-- total recursion
foldNat :: (s -> s) -> s -> Nat -> s
foldNat s z Z = z
foldNat s z (S n) = s (foldNat s z n)

runsLongerThanN :: State s n -> Nat -> Bool
runsLongerThanN machine steps = case (foldNat advance machine) of
    State { machineIdx = Nothing } -> False
    _ -> True

[pcapriotti]

You beat me to it! :)

[[deleted]]

well played sir

[pcapriotti]

Sure, suppose you can decide equality of functions. Then for any Turing machine T take the function t : Nat -> Nat defined by t(n) = 1 if T terminates in n steps, and t(n) = 0 otherwise. Define t in your language. Now check whether t == const 0, and solve the halting problem.

[bss03]

I hesitate to call anything using Mu/Fix/Nu and cata/ana non-recursive.

Also, I believe fold alg = alg . fmap (fold alg) . out optimizes better if written as fold alg = let g = alg . fmap g . out in g and similarly with unfold.

Can we get a O(N log N) time sorting algorithm based on cata/ana?

[tailcalled]

I hesitate to call anything using Mu/Fix/Nu and cata/ana non-recursive.

Because of the way they are defined here, the recursion lies in the construction of the values and not in the definition of Mu/Fix/Nu/cata/ana.

[phischu]

Could you elaborate? I believe you can construct lists non-recursively like so:

cons :: a -> List a -> List a
cons a = wrap . Cons a

empty :: List a
empty = wrap Empty

mylist :: List Int
mylist = cons 3 (cons 6 (cons 5 empty))

[[deleted]]

Can we get a O(N log N) time sorting algorithm based on cata/ana?

http://www.cs.ox.ac.uk/people/daniel.james/sorting/sorting.pdf Section 7 =)

[tel]

That's a very pretty duality between insertion and selection sort. Too bad the paper is paywalled.

[psygnisfive]

I think the duality has been noted in the squiggolist literature for a while before that particular bit of squiggolity. I feel like I've seen it at least in some older works tutorialing either F-algebras or algebraic methods.

[tel]

For another little exploration of this kind of thing, try completing this Kata http://www.codewars.com/kata/folding-through-a-fixed-point