Zulip Chat Archive

Stream: lean4

Topic: Herbrand's Unification Theorem


Julien Marquet (Nov 12 2021 at 20:33):

Hello,

I proved (over the course of a 2 weeks' ~speedrun) Herbrand's [1] unification theorem [2] in the special case of the terms that appear in GoI flows [3] [4].

See the statement here !


I am interested in formalizing flows [3] [4], which are object that allow to present low-level computations in a satisfactory way (up to my understanding).
The first step towards this goal is this theorem that I proved.

I tried to formalize the theorem as quickly as possible, so the code is far from being perfect... but I will (at some point within the next 9 months) get back to it and clean it up.

There may be some things around here (nontrivial inductions, finiteness and lower bounds) that may be relevant for mathlib4 if they were cleaned up a bit, I'm willing to spend some time at some point in a fairly near future on it if you think this is worth the effort.

The repo is here : https://github.com/thejohncrafter/flows !


[1] : Lectures on Herbrand, with historical notes https://arxiv.org/pdf/0902.4682.pdf

[2] : Jacques Herbrand's dissertation (in French), pp. 96-97

[3] : Geometry of Interaction analyzed with flows https://www.normalesup.org/~bagnol/notes/goi-torino.pdf

[4] : Notes on unification using flows (in French) https://www.normalesup.org/~bagnol/notes/unification.pdf (in French)

Franz Kronseder (Nov 13 2021 at 12:33):

Hello Julien.Marquet :) Thank you for contributing this Herbrand-Stuff here ...
FYI I have been passionate amateur consumer of the leanprover-zulip-chats about MathLib-Worlds since XMas-2020...
I remember hearing abt Herbrand-Universes while learning "Programming in Prolog" during my TUM-Inf years in the early 1980s.
... looking fwd to refreshing my school-french reading-skill by reading your (in French) URLs ...
Cheers from Muenchen-Moosach, Franz


Last updated: Dec 20 2023 at 11:08 UTC