Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Generators, inductive types and fixpoints in linear logic

Andrew Cann (Nov 07 2020 at 08:01):

I've noticed that you can define least and greatest fixpoints in linear logic in terms of the exponentials:

μα.F[α] = ∀α. α ⅋ ?(¬α ⊗ F[α])
να.F[α] = ∃α. α ⊗ !(¬α ⅋ F[α])

For instance, Nat can be defined as:

Nat
    = μα.(1 + α)
    = ∀α. α ⅋ ?(¬α ⊗ (1 + α))

This is probably easier to see if you look at its dual:

¬Nat
    = να.(⊥ & α)
    = ∃α. α ⊗ !(¬α ⅋ (⊥ & α))

To eliminate this you need to eliminate the α which you can only do by calling the function ¬α ⅋ (⊥ & α). You then have a choice of stopping by taking the ⊥ or repeating by taking the α which you then have to put back into the function again. In other words you eliminate ¬Nat by feeding it a Nat.

μ and ν types behave like additive connectives - you match on an inductive type by giving it a generator which folds over the tree, and you match on a generator by giving it a tree representing the path to take through the generator. They also have the property that:

μα.α = 0
να.α = ⊤

I feel like maybe there should be two more fixpoint-like type constructors which behave like multiplicative connectives. If we call them φ and ψ, these would have the property that:

φα.α = ⊥
ψα.α = 1

The intro rules for these types would have to mirror each other such that the pattern syntax for φ would be the term syntax for ψ and vice-versa.

Does anyone know what these fixpoints could be? Is there any other way to define the "fixpoint" of a functor in linear logic such that you get these properties? I'm interested in this because trees and generators seem like pretty essential features of a programming language, and they also (kind-of) generalise ! and ?. I'm trying to design a programming language based on linear logic and I'm considering having μ and ν types instead of or in addition to ! and ?. But there's still a lack of expressivity that I'm trying to plug by looking for symmetries. Since μ and ν can be defined in terms of ! and ?, maybe φ and ψ can be defined in terms of ¡ and ¿? Or not. I'm really clutching at straws here. Any feedback would be appreciated :)

sarahzrf (Nov 07 2020 at 08:22):

these are gonna be church encodings right?

Andrew Cann (Nov 07 2020 at 08:34):

Hmm, how do you mean? I'm trying to design a language around linear logic which I talk about a bit in my previous post here. I'm not sure how or if it's possible to reduce this language to vanilla lambda calculus though.

Kenji Maillard (Nov 07 2020 at 09:25):

I concur with @sarahzrf that it looks like a form of church encoding, and I think a variant $\mathbb{N} = \forall \alpha, \alpha \to !(\alpha \to \alpha) \to \alpha$ is mentioned in Girard's original article on linear logic as a way to encode natural numbers (and further detailed later in the articles about light linear logics where this encoding crucially needs to be refined). Though you might have less negations in the way..

You might be interested in this outstanding PhD thesis by Amina Doumane exploring in depth how to add primitively least and greatest fixpoints to linear logic.

James Wood (Nov 07 2020 at 11:51):

Notice that ∀α. α ⅋ ?(¬α ⊗ F[α]) is the same as ∀α. !(F[α] ⊸ α) ⊸ α, which looks about right.