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: learning: questions

Topic: How to model judgements of equality in inference rules?

Mike Stay (Dec 20 2024 at 21:54):

I would like to model judgements of equality. The inference rule expressing subject reduction, i.e. that terms preserve their types under reduction, uses such judgements.

Γ ⊢ A: B    Γ ⊢ C: ⊤     Γ ⊢ s(C) = A    Γ ⊢ t(C) = A'    Γ ⊢ A': B'
—————————————————————————————————————————————————————————————————————
Γ ⊢ A: B'

where B, B' are types refining the sort of terms and ⊤ is the type that trivially refines the sort of reductions. The function symbols s and t pick out the source and target of a reduction, respectively.

In the absence of the equality judgements, I could model this as a natural transformation between profunctors. What's the right way to model the equality judgements?

Mike Stay (Dec 20 2024 at 21:54):

Details:

I'm modeling lambda calculus using a graph-structured lambda theory. I'll use a reduction strategy where we only reduce lambdas in the head position of an application, resulting in weak head normal form. (Modeling lambda calculus in a lambda theory is kind of silly, but it lets me reason about the number of steps in a reduction and lets the theory handle bound variables and substitution.)

Mike Stay (Dec 20 2024 at 21:55):

• The graph structure
  • One generating sort T for terms
  • One generating sort R for reductions
  • Two generating morphisms s, t: R -> T for the source and target of a reduction
• Two generating function symbols for terms
  • App: T x T -> T
  • Lam: (T -> T) -> T
• Two generating function symbols for reductions
  • Beta: ((T -> T) x T) -> T
  • Head: R x T -> R
• Two equations for the source and target of Beta
  • s(Beta(a, b)) = App(Lam(a), b)
  • t(Beta(a, b)) = eval(a, b)
• Two equations for the source and target of Head
  • s(Head(a, b)) = App(s(a), b)
  • t(Head(a, b)) = App(t(a), b)

Ryan Wisnesky (Dec 20 2024 at 23:34):

Is modeling this without pro-functors an option? Just treating G |- t1 = t2 : T to mean that morphisms G |- t1 : T and G |- t2 : T are equal? A priori I'd expect most inference rules not to turn into equations in a lambda theory, but into more general formulae (implications, etc).

Mike Stay (Dec 20 2024 at 23:48):

Most inference rules actually turn out to be natural and dinatural transformations between profunctors. For example,

Γ ⊢ v: A    Γ, x: A ⊢ B: C
——————————————————————————
Γ ⊢ B[v/x]: C

is natural in Γ and C and dinatural in A. The dinatural part is α: F => G, where

F, G: T^op x T x T^op x T -> Set
F = (Γ, A, A', C) --∆AA'C--> (Γ, Γ, A, A', C) --iso--> ((Γ, A), ((Γ, A'), C)) --hom x hom--> Γ ⊢ A    Γ, A' ⊢ C
G = (Γ, A, A', C) --ΓδδC--> (Γ, 1, 1, C) --iso--> (Γ, C) --hom--> Γ ⊢ C
α(m, n) = n ⚬ (Γ x m)

and the commuting hexagon says that given f:A -> A', h: Γ -> A, j: Γ, A' -> C,

(j ⚬ Γh) ⚬ Γf = j ⚬ Γ(h ⚬ f).

Mike Stay (Dec 21 2024 at 08:15):

In this particular case, I guess I can write something like

Γ ⊢ s(A): B    Γ ⊢ t(A): B'
———————————————————————————
Γ ⊢ s(A): B'

But I'd still like to understand what categorical machinery would let me say Γ ⊢ x(A) = y(B).