Relational calculus with semantics in a Z/2-graded "alternating multicategory"

alternating.txt

Relational calculus with hopes to give semantics in a kind of "alternating multicategory".

I want to work with the exterior algebra ⋀ 𝔽₂[S] (or possibly formal power series ⋀ 𝔽₂[[S]] or algebraic power series ⋀ 𝔽₂(S)) as a nice way of working with set-set apartness relations and denotational semantics.

I want a kind of operad for my set of terms S that composes well with the exterior algebra ⋀ 𝔽₂[S]. I think I require some form of "super operads" but finite fields are already really confusing. Not really happy that enriching over super vector spaces seems to be required.

I suspect you basically want a kind of graded closed semi-additive category but maybe a little weaker.

Symmetry is a natural isomorphism.

s: C(A ⊗ B, -) → C(B ⊗ A, -)

Antisymmetry is a natural isomorphism with some kind of sign change such as variance.

a: C(A ⊗ B, -) → C(-, B ⊗ A)

But I think antisymmetry implies a kernel which is really all you need.

Not really sure of the connection between the Hodge Star and kernels.

Bleh, I think I need to go back to uglier linear logic to keep antisymmetry. Typing with leftovers 

DEFINE

∅ ≡ ker x. x
e₀ ⊖ e₁ ≡ (ker x. x [y. y; ∅ ⇔ z. z; ∅]) [x. x; e₀ ⇔ y. y; e₁]
ival ≡ ker x. x [y. y; ∅ | z. z; ∅]
e₀ ∨ e₁ ≡ ival [x. x; e₀ | y. y; e₁]
e₀ ∧ e₁ ≡ (e₀, e₁) .π₁ 
{ x | e₀ = e₁ } ≡ ker x. e₀ ⊖ e₁
ε x. e ≡ { x | e = i₁ • }
assert e ≡ e [x. x; • | y. y; ∅]

Something along these lines seems right but probably not this exact thing.
ω ≡ ker x. ⋆x

You probably want the following but I can't figure out the eliminator.

q₁ e ≡ { x | x .π₁ = e }
q₂ e ≡ { x | x .π₂ = e }

You want that contravariant variables transform differently under permutation...

λ x y. (⋆x, y) = -λ y x. (⋆x, y)

e ::=
    | xₖ | ⋆xₖ | ker x. e
    | • | e₀; e₁
    | q₁ e | q₂ e | e₀ [x. e₁ ⇔ y. e₂]
    | e₀ # e₁ | e₀ to x y. e₁
    | i₁ e₀ | i₂ e₁ | e₀ [x. e₁ "|" y. e₂]
    | e₀, e₁ | e₀ .π₁ | e₁ .π₂
t ::= 𝔻 | 1 | t₀ ⅋ t₁ | t₀ & t₁ | t₀ ⊗ t₁ | t₀ ⊕ t₁
Γ ::= • | Γ, x: t
u ::= s | f
σ ::= • | σ, u

I really should use a different symbol for use annotations than is used for environments. Also the double arrow conflicts with small step semantics.

Typing judgements

x: t ∈ Γ ⊠ σ
────────────    ⋆
Γ ⊠ σ ⇒ σ\x ⊢ ⋆x: t

Γ, x: t₀ ⊠ σ₀, f ⇒ σ₁, s ⊢ e: t₁
──────────────────     ker
Γ ⊠ σ₀⇒σ₁ ⊢ ker x: t. e: t

───────────    1-intro
Γ ⊠ σ₀ ⇒ σ₁ ⊢ •: 1

Γ ⊠ σ₀ ⇒ σ₁ ⊢ e₀: 1
Γ ⊠ σ₁ ⇒ σ₂, ⊢ e₁: t
───────────    1-elim
Γ ⊠ σ₀ ⇒ σ₂ ⊢ e₂: t

Γ ⊠ σ₀⇒ σ₁ ⊢ e: t₀
────────────────    ⊕-intro₁
Γ ⊠ σ₀ ⇒ σ₁ ⊢ i₁ e: t₀ ⊕ t₁

Γ ⊠ σ₀ ⇒ σ₁ ⊢ e: t₁
────────────────    ⊕-intro₂
Γ ⊠ σ₀ ⇒ σ₁ ⊢ i₂ e: t₀ ⊕ t₁

Γ ⊠ σ₀ ⇒ σ₁ ⊢ x: t₀. e₀: t₀ ⊕ t₁
Γ, x: t₀ ⊠ σ₁, f ⇒ σ₂, s ⊢ e₁: t₂
Γ, y: t₁ ⊠ σ₂, f ⇒ σ₃, s ⊢ e₂: t₂
───────────────────    ⊕-elim
Γ ⊠ σ₀ ⇒ σ₃ ⊢ e₀[x. e₁ | y. e₂]: t₂

Γ ⊠ σ₀⇒ σ₁ ⊢ e: t₀
────────────────    ⅋-intro₁
Γ ⊠ σ₀ ⇒ σ₁ ⊢ i₁ e: t₀ ⅋ t₁

Γ ⊠ σ₀⇒ σ₁ ⊢ e: t₁
────────────────    ⅋-intro₂
Γ ⊠ σ₀ ⇒ σ₁ ⊢ i₂ e: t₀ ⅋ t₁

Γ ⊠ σ₀ ⇒ σ₁ ⊢ x: t₀. e₀: t₀ ⅋ t₁
Γ, x: t₀ ⊠ σ₁, f ⇒ σ₂, s ⊢ e₁: t₂
Γ, x: t₁ ⊠ σ₁, f ⇒ σ₂, s ⊢ e₂: t₂
───────────────────    ⅋-elim
Γ ⊠ σ₀ ⇒ σ₂ ⊢ e₀[x. e₁ ⇔ y. e₂]: t₂

Γ ⊠ σ₀ ⇒ σ₁ ⊢ e₀: t₀
Γ ⊠ σ₀ ⇒ σ₁ ⊢ e₁: t₁
────────────────     &-intro
Γ ⊠ σ₀ ⇒ σ₁ ⊢ e₀, e₁: t₀ & t₁

Γ ⊠ σ₀ ⇒ σ₁ ⊢ e: t₀ & t₁
──────────────    &-elim₁
Γ ⊠ σ₀ ⇒ σ₁ ⊢ e .π₁: t₀

Γ ⊠ σ₀ ⇒ σ₁ ⊢ e: t₀ & t₁
──────────────    &-elim₂
Γ ⊠ σ₀ ⇒ σ₁ ⊢ e .π₂: t₁

Γ ⊠ σ₀, f ⇒ σ₁, s ⊢ e₀: t₀
Γ ⊠ σ₁, f ⇒ σ₂, s ⊢ e₁: t₁
─────────────────────    ⊗-intro
Γ ⊠ σ₀ ⇒ σ₂ ⊢ x: t₀. e₀ # e₁: t₀ ⊗ t₁

Γ ⊠ σ₀ ⇒ σ₁ ⊢ x: t₀. e₀: t₀ ⊗ t₁
Γ, x: t₀, y: t₁ ⊠ σ₁, f ⇒ σ₂, s ⊢ e₁: t₂
─────────────────────    ⊗-elim
Γ ⊠ σ₀ ⇒ σ₂ ⊢ e₀ to x y. e₁: t₂

x: t ∈ Γ ⊠ σ
───────────    var
Γ ⊠ σ ⇒ σ\x ⊢ x: t

Denotational Semantics. There's some topology stuff I don't get and it gets far too confusing nesting sets like that.

Maybe try an interpretation in Span?

I need to prove this is linear and finite.

⟦t₀ & t₁⟧ = ⟦t₀⟧ × ⟦t₁⟧ 
⟦t₀ ⊗ t₁⟧ = ⟦t₀⟧ × ⟦t₁⟧ 
⟦t₀ ⅋ t₁⟧ = ⟦t₀⟧ + ⟦t₁⟧
⟦t₀ ⊕ t₁⟧ = ⟦t₀⟧ + ⟦t₁⟧ 

⟦-⟧:
  { e: Γ ⊠ σ₀ ⇒ σ₁ ⊢ e: t } →
  (∀ x. ℙ(⟦Γₓ⟧)) → ℙ(ℙ(⟦t⟧))

⟦x⟧(σ, C) = C ⊆ σₓ
⟦⋆x⟧(σ, C) = σₓ ⊆ C
⟦ker x. e⟧(σ, C) = ⟦e⟧(C :: σ, λ A, ∀ a. a ∉ A)
⟦e₀, e₁⟧(σ, C) =
    ⟦e₀⟧(σ, λ A, 
    ⟦e₁⟧(σ, λ B, 
       ∀ a ∈ A.
       ∀ b ∈ B.
       i₁ a ∈ C ⊕ i₂ b ∈ C))
⟦e .π₁⟧(σ, C) =
   ⟦e⟧(σ, λ A,
       ∀ a ∈ A.
       match a with
       | i₁ a' => a' ∈ C
       | i₂ _ => ⊥
       end)
⟦e₀ # e₁⟧(σ, C) =
    ⟦e₀⟧(σ, λ A,
    ⟦e₁⟧(σ, λ B,
       ∀ a ∈ A.
       ∀ b ∈ B.
       (a, b) ∈ C))
⟦e₀ to x y. e₁⟧(σ, C) =
    ⟦e₀⟧(σ, λ A,
    ⟦e₁⟧({ a | (a, b) ∈ A } :: { b | (a, b) ∈ A } :: σ, C))
⟦i₁ e⟧(σ, C) =
    ⟦e⟧(σ, λ A,
        ∀ a ∈ A.
        i₁ a ∈ C)
⟦e₀ [x. e₁ | y. e₂]⟧(σ, D) =
   ⟦e₀⟧(σ, λ A,
   ⟦e₁⟧({ a | i₁ a ∈ A } :: σ, λ B,
   ⟦e₂⟧({ a | i₂ a ∈ A } :: σ, λ C,
       ∀ b ∈ B.
       ∀ c ∈ C.
       b ∈ D ⊕ c ∈ D))
⟦q₁ e₀⟧(σ, C) =
    ⟦e₀⟧(σ, λ A,
        ∀ a ∈ A.
        a ∈ { a | (a, b) ∈ C }))
⟦e₀ [x. e₁ ⇔ y. e₂]⟧(σ, D) =
   ⟦e₀⟧(σ, λ A,
   ⟦e₁⟧({ a | (a, b) ∈ A } :: σ, λ B,
   ⟦e₂⟧({ b | (a, b) ∈ A } :: σ, λ C,
       ∀ b ∈ B.
       ∀ c ∈ C.
       b ∈ D ⊕ c ∈ D))