3 ms·
Kauffman has some papers with Buliga about graphical lambda calculus -- it seems like it's working with the string diagrams for a reflexive category, but with s
by kmill 6y ago
Kauffman has some papers with Buliga about graphical lambda calculus -- it seems like it's working with the string diagrams for a reflexive category, but with some extra goodies from an algebraic structure.
I was about to say "oh, you found a quandle/rack in the lambda calculus," but it seems you're already aware of this, given some of the filenames in your repository :-) In the Buliga/Kauffman papers, there are sections about representations of knot crossings as lambda calculus, which presumably forms a quandle (actually, probably a rack). Could you direct me to how your @ operation works? This seems very interesting.
I recently added quandles/racks to mathlib[1], the Lean standard math library. I think mathlib has some lambda calculus formalization, so it might be interesting adding a quandle instance for your operation.
[1] https://github.com/leanprover-community/mathlib/blob/master/src/algebra/quandle.lean https://github.com/leanprover-community/mathlib/blob/master/...
- deleted 6y ago[deleted]
- zitterbewegung 6y agoI tried to work with Bulgia and Kauffman to move forward on that project but it was too complicated and also learning awk is very painful.
- zitterbewegung 6y agoI have encountered your GitHub code (specifically the software you use to draw knots). The lambda calculus with the self distributive magma basically would have all of the axioms of the lambda calculus but also with every valid statement in lambda calculus you also add the left self distributively law. This was a simplification of the project due to time constraints. The original goal were to have all of the quandle operations to operate on every welf formed statement that would be a rewriting system. https://ncatlab.org/nlab/show/self-distributive+operation https://ncatlab.org/nlab/show/self-distributive+operation (a (b c)) => (a b) (a c) So lets say we have the following church numeral. λf.λx.f (f (f x)) We would be able to do an operation using the self-distributive operation λf.λx.f (f (f x)) => λf.λx.f (f f) (f x) This is a bit hand-wavy though.