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: event: ACT@UCR

Topic: May 20th: Gordon Plotkin

John Baez (May 18 2020 at 22:13):

In the eighth talk of the ACT@UCR seminar, Gordon Plotkin will tell us about partial differentiation, viewed as a logical theory.

He will give his talk on Wednesday May 20th at 5 pm UTC, which is 10 am in California, or 1 pm on the east coast of the United States, or 6 pm in England. It will be held online via Zoom, here:

https://ucr.zoom.us/j/607160601

You can see his slides here.

• Gordon Plotkin, A complete axiomatisation of partial differentiation.

Abstract. We formalise the well-known rules of partial differentiation in a version of equational logic with function variables and binding constructs. We prove the resulting theory is complete with respect to polynomial interpretations. The proof makes use of Severi’s theorem that all multivariate Hermite problems are solvable. We also hope to present a number of related results, such as decidability and Hilbert-Post completeness.

Cody Roux (May 18 2020 at 22:15):

Sweet!

Cody Roux (May 20 2020 at 17:56):

Ok I have a second question, but I don't want to overwhelm the talk: Is there a way to orient all the equations, except the commutativity one, and get a normalizing rewrite system?

Philip Zucker (May 20 2020 at 17:57):

https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/book.html This is the classical mechanics book referenced. It's available free online

Cody Roux (May 20 2020 at 17:57):

You could also give a "canonical" ordering of the variables and then order the commutativity one so that the small variables "go outward"

Cody Roux (May 20 2020 at 17:59):

@Gordon Plotkin can you see a link to this comment?

John Baez (May 20 2020 at 17:59):

Hi, Gordon!

Gordon Plotkin (May 20 2020 at 18:03):

OK ask a question

John Baez (May 20 2020 at 18:03):

So Cody asked: "I have a second question, but I don't want to overwhelm the talk: Is there a way to orient all the equations, except the commutativity one, and get a normalizing rewrite system?"

Gordon Plotkin (May 20 2020 at 18:05):

Hmm, it is not simple, there are also the ring axioms, and it won't be normalising (think about polynomials which don't have natural normal forms)

Jonathan Gallagher (May 20 2020 at 18:06):

Hi Cody! For the notation for CDCs by Blute, Cockett, Seely, a rewriting system is possible. You do get sort of rewriting system, but you need to make the chain rule oriented the "wrong way" That is the chain rule becomes an expansion rewrite, and you get what's known as an expansion reduction system. This normalizes in the sense of an expansion reduction system, in fact in that language it's strongly normalizing. It's also Church-Rosser modulo the symmetry axiom and the axioms of a commutative monoid. Sadly, I don't think this has been published.

Cody Roux (May 20 2020 at 18:06):

How about with Grobner orderings?

Gordon Plotkin (May 20 2020 at 18:06):

For addition you also have to combine the axiom with the chain rule. canonicalisation is trying to do something of this kind

Cody Roux (May 20 2020 at 18:06):

Jonathan Gallagher said:

Hi Cody! For the notation for CDCs by Blute, Cockett, Seely, a rewriting system is possible. You do get sort of rewriting system, but you need to make the chain rule oriented the "wrong way" That is the chain rule becomes an expansion rewrite, and you get what's known as an expansion reduction system. This normalizes in the sense of an expansion reduction system, in fact in that language it's strongly normalizing. It's also Church-Rosser modulo the symmetry axiom and the axioms of a commutative monoid. Sadly, I don't think this has been published.

Cool!

Cody Roux (May 20 2020 at 18:07):

@Gordon Plotkin thanks! That makes sense. It's natural to wonder what the pragmatic decision procedure would be. It sounds like it's this stratified interpolation trick right now.

Gordon Plotkin (May 20 2020 at 18:08):

Thats very nice for CDCs!

Christian Williams (May 20 2020 at 18:09):

So, did you present the "theory of differentiation" as a second-order algebraic theory (Fiore et al)? I thought I heard you say toward the end that it wasn't fully second-order, but I'm not sure what you meant.

John Baez (May 20 2020 at 18:10):

I think Gordon said he was deliberately avoiding second-order approach. Right?

Gordon Plotkin (May 20 2020 at 18:11):

I did present it as a theory in the sense of Fiore et al, I was speaking vaguely at the end, contrasting with a predicate calculus theory with comprehension

John Baez (May 20 2020 at 18:11):

Now I'm confused.

John Baez (May 20 2020 at 18:12):

(Or rather, I always was but now I realize it.)

Nathanael Arkor (May 20 2020 at 18:12):

If I understood correctly, the calculus is a one-sorted second-order algebraic theory à la Fiore–Plotkin–Turi's Abstract Syntax and Variable Binding.

John Baez (May 20 2020 at 18:13):

Oh, cool.

Nathanael Arkor (May 20 2020 at 18:13):

By using second-order theories instead of some lambda abstraction, you can interpret the calculus in more models (e.g. categories that aren't cartesian-closed).

Christian Williams (May 20 2020 at 18:13):

Yes, that last part of the discussion went by too quickly for me. Is the main contrast that predicates with comprehension undecidable? But it's still second-order, right -- so I'm wondering what exactly makes it so expressive. (Maybe there are other factors besides expressiveness, I don't know about this stuff.)

Gordon Plotkin (May 20 2020 at 18:15):

You understand correctly, Nathanael.
Re second order , I am finding it difficult to sort out the different senses of the word in real time, they will include second-order logic, concrete and nonconcrete models (of the equational theory) and standard and non-standard models of the logic.

Cody Roux (May 20 2020 at 18:16):

Christian Williams said:

Yes, that last part of the discussion went by too quickly for me. Is the main contrast that predicates with comprehension undecidable? But it's still second-order, right -- so I'm wondering what exactly makes it so expressive. (Maybe there are other factors besides expressiveness, I don't know about this stuff.)

Expressive can mean "can talk about many things" or "can prove many things". In general, logics with binding constructs are of the first sort, and HOL is of the second sort.

Christian Williams (May 20 2020 at 18:17):

Where were the slides posted, by the way?

Cody Roux (May 20 2020 at 18:18):

Here's a theorem that I use a lot for intuition: Martin-Lof type theory without universes is a conservative extension of first-order logic, even though it can quantify over arbitrary function spaces.

Jonathan Gallagher (May 20 2020 at 18:18):

http://math.ucr.edu/home/baez/mathematical/ACTUCR/Plotkin_Partial_Differentiation.pdf

Gordon Plotkin (May 20 2020 at 18:19):

Re implications
conjunctions of e=e''s implies e'' = e'''
true over the smooth functions they must surely be undecidable, as partial differential equations can be equations in this calculus.

Christian Williams (May 20 2020 at 18:25):

I'm trying to understand the interpretation of $\mathrm{PDiff}(x.e_0,e_1)$. What does it mean for $e_1$ be a compound expression rather than a variable?

Jonathan Gallagher (May 20 2020 at 18:26):

IIRC a restriction on PDEs to "primitive PDEs" i.e. Shannon's GPAC, were shown to be equivalent to Turing machines by a polynomial time reduction.

Christian Williams (May 20 2020 at 18:27):

Oh, I can see through the example theorem for chain rule.

John Baez (May 20 2020 at 18:27):

A class of PDE equivalent to Turing machines - cool!

Gordon Plotkin (May 20 2020 at 18:29):

Jonathan, I would love a reference, please.

Christian Williams (May 20 2020 at 18:30):

Can the theory of differentiation be understood as a fragment of the internal logic of cartesian differential categories?

Jonathan Gallagher (May 20 2020 at 18:31):

See theorem 14 -- 17 of https://reader.elsevier.com/reader/sd/pii/S0885064X07000246?token=72278894AD328E44CE53742FB6E94226C9198B12975776D18A7CA56CE853A273EADE09C6DEE593632B05F585924B3BC5

Gordon Plotkin (May 20 2020 at 18:35):

Thanks, Jonathan.
Christian, if by internal logic we take it to be the second-order theory I have at the end (which should be essentially equivalent to the type theory Jonathan mentioned), then it can be interpreted in my second-order theory, by interpreting the single sort there as a product of sorts of my theory (this just formalises the definitions of Jacobians). I think the converse may not hold (ie I think it is not a fragment, as you asked)

John Baez (May 20 2020 at 18:37):

I think I'll sign off, Gordon. I'm a bit out of my depth here. Thanks for a great talk!

Gordon Plotkin (May 20 2020 at 18:39):

You are welcome, John. I will sign off too, if there are no more questions. Thanks everyone!

Jonathan Gallagher (May 20 2020 at 18:39):

Thank you for the talk!

Jonathan Gallagher (May 20 2020 at 18:40):

Re the theory of differentiation: it may a fragment of the theory used by Wolfgang Betram. http://www.iecl.univ-lorraine.fr/~Wolfgang.Bertram/simfin.pdf

John Baez (May 20 2020 at 22:51):

You can see Gordon's slides here, or download a video of his talk here, or watch his video here:

https://www.youtube.com/watch?v=j_w6GNUIQDo&w=560&h=315

Nathanael Arkor (May 20 2020 at 23:18):

@Gordon Plotkin: you said you were looking for examples in mathematics of operators that take multiple binding arguments? One (multisorted) example is the case-splitting operation in the STLC with sums, where we have an operator case : Sum(A, B), (A)C, (B)C -> C.

Nathanael Arkor (May 20 2020 at 23:19):

(I missed this comment whilst watching earlier.)

Erik Meijer (May 21 2020 at 02:06):

Since people were wondering about applications of derivatives of boolean functions https://pdfs.semanticscholar.org/a9c8/7568463a5ce8c2cd15ec17e9a54e1158db2b.pdf
https://books.google.com/books?id=DgC7IuDGvMQC&printsec=copyright#v=onepage&q&f=false

John Baez (May 21 2020 at 20:40):

Great! I'm gonna have to learn about this. I want to freak people out by taking the derivative of "and".

sarahzrf (May 21 2020 at 22:03):

it better obey a leibniz rule or i want my money back

sarahzrf (May 21 2020 at 22:05):

actually wait maybe it's xor that would obey a leibniz rule

Jacques Carette (May 21 2020 at 22:10):

There are all sorts of interesting things about boolean derivatives in "Conservative retractions of propositional logic theories by means of boolean derivatives. Theoretical foundations" https://core.ac.uk/download/pdf/158965834.pdf

John Baez (May 21 2020 at 22:11):

Hey, that looks nice!

Philip Zucker (May 22 2020 at 13:08):

So would a fair characterization of the talk (for a non logician) be that one can decide whether a single equality involving partial derivatives, +, *, composition, and uninterpreted smooth function symbols, is a consequence of the basic rules of arithmetic and differentiation by considering interpretations of those functions as polynomials of bounded degree? And that I can't use the method to ask questions like is y'' = y' a consequence of y' = y?