# OK to post homework
# Robert Dougherty-Bliss
# 2021-04-03
# Assignment 18

# We need to recreate some boolean lattice code. That's great, because I don't
# actually know very much about lattices.

### BEGIN SPERNER'S LEMMA RANT ###

# Sperner's lemma basically says this: The largest antichain in a symmetrically
# decomposable lattice is the collection of middle elements. In the boolean
# lattice on [n], that's just the (n / 2)-element subsets.

# A ranked lattice is a lattice where every element has an integer "rank" which
# satisfies rank(A) < rank(B) if A < B and rank(B) = rank(A) + 1 if B is a
# successor of A. In the boolean lattices, the rank is the cardinality of the
# subset.

# Distinct elements of rank R are not comparable. If rank(A) = rank(B), and A
# and B are comparable, then A >= B and A <= B, so A = B. Thus, the elements of
# rank R form an antichain. This gives us a "cheap" way to form antichains.

# In the boolean lattice, the "middle" elements of rank n / 2 are the biggest
# such collection, having size binomial(n, n / 2). Thus the largest antichain
# in the boolean lattice has size *at least* binomial(n, n / 2).

# A symmetric chain decomposition (SCD) is a decomposition of a lattice into a
# disjoint union of chains formed by adding successors.

# Sperner's lemma: If a lattice has a symmetric chain decomposition, then every
# antichain contains all elements of "middle" rank.

# Every symmetric chain satisfies start rank + end rank = n, so we must have

#       start rank <= n / 2

# and

#       end rank >= n / 2,

# meaning that there is at least one element of rank floor(n / 2) in the chain.
# Since these elements are not comparable, there is also at *most* one middle
# element in the chain, so there must be exactly as many chains as there are
# middle elements.

# Now, take an arbitrary antichain in the lattice. Each element must belong to
# distinct chains of the SCD, or else they would be comparable. Thus the
# antichain is no larger than the number of chains, which equals the number of
# middle elements.

### END SPERNER'S LEMMA RANT ###

with(combinat):
with(ListTools):

# Greedily construct a SCD of the boolean lattice on [n].
Aigner := proc(n)
    local chains, L, nonEmptyLevel, chain, currentLevel:
    chains := []:
    L := [seq(choose(n, k), k=0..n)]:

    nonEmptyLevel := 0:

    while nonEmptyLevel < n do
        chain := []:
        for currentLevel from nonEmptyLevel to n - nonEmptyLevel do
            # Find the first in the current level that contains us.
            if nops(chain) > 0 then
                k := findSubset(chain[-1], L[currentLevel + 1]):
                if k = -1 then
                    ERROR("failed to choose successor");
                fi:
            else
                k := 1:
            fi:

            chain := [op(chain), L[currentLevel + 1][k]]:
            L[currentLevel + 1] := [op(L[currentLevel + 1][..k-1]), op(L[currentLevel + 1][k+1..])]:

            if nonEmptyLevel = currentLevel then
                while nonEmptyLevel < n and nops(L[nonEmptyLevel + 1]) = 0 do
                    nonEmptyLevel := nonEmptyLevel + 1:
                od:
            fi:
        od:

        chains := [op(chains), chain]:
    od:
end:

findSubset := proc(A, Ls)
    for k from 1 to nops(Ls) do
        if andmap(x -> member(x, Ls[k]), A) then
            return k
        fi:
    od:

    return -1:
end:

# Dr. Z's suggestion from lecture: For each chain in SCD(n - 1), copy the last
# link and put n into it. Also insert n into the first link and chop off the
# last element.

SCD := proc(n)
    if n = 0 then
        return {[[]]}:
    fi:

    oldChains := SCD(n - 1):
    chains := {}:

    for chain in oldChains do
        last := [op(chain), [op(chain[-1]), n]]:
        first := [seq([op(link), n], link in chain[..-2])]:
        if nops(first) > 0 then
            chains := {op(chains), last, first}:
        else
            chains := {op(chains), last}:
        fi:
    od:
end:

# SCD is *much* faster for small n!

# Here's some code that investigates why:

with(CodeTools[Profiling]):

Profile(Aigner):
Profile(SCD):

Aigner(12):
SCD(12):

PrintProfiles(Aigner);
PrintProfiles(SCD);

# 80% of the Aigner runtime is brute-force searching for a lexicographic
# successor.

# However, even if we were to reduce that to instantaneous, Aigner would still
# be about 5 times slower than than SCD. There's just a lot of logic going on
# there.