Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

Atrium > Mathematics, Physics & Philosophy: Cactus Language & Differential Logic

Bottom of Page

1 to 7 of 7

  1.  
    • CommentRowNumber1.
    • CommentAuthorJonAwbrey
    • CommentTimeSep 10th 2009
    DC: Explain to us if you would what cactus language has to do with anything else in nLab.

    DC: And what does differential logic have to say to the n-category project?

    Questions of relevance are always in order, but they can't always be answered in sound-bytes. My feeling is that the best way to show the desired connections is simply to keep developing the material to the point where its bearing becomes clear.

    Okay, that ship has sailed — so I'll try to give a prospectus here.

    2-night or 2-morrow …

    Jon
    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2009

    Thanks, Jon. As you say, it is good ‘to keep developing the material to the point where its bearing becomes clear’, and I'm happy that you intend to do that, but it will also be nice to see the big picture. (^_^)

    • CommentRowNumber3.
    • CommentAuthorJonAwbrey
    • CommentTimeSep 11th 2009
    The way I see it, the Big Picture is something like "applying the technologies of communication and computation to the support of inquiry". And I certainly see reasonable facsimiles of that vision articulated throughout the n-Cafe and TWF — indeed, it was that spirit of venturous but rigorous intellect that drew me to these sites in the first place

    But we seem to be sweating the small stuff now …

    That's okay, per angusta ad augusta, ad astra per aspera, no pain no gain, and all that rot.

    If you look at things recursively, as I tend to do, you have to ask yourself the ⟙↓ question:

    What's the relation between the Big Picture and the small stuff?

    Jon
    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeSep 11th 2009

    The more you talk without saying anything, the more I am in sympathy with David.

    • CommentRowNumber5.
    • CommentAuthorJonAwbrey
    • CommentTimeSep 11th 2009
    I'll discuss these topics in tandem, because today I see them as intimately related, even though it was only recently that I tumbled to the fact with any kind of full awareness.

    I spent the better part of my so-called "spare time" in the 80's writing a program with a "learning module" (LM) and a "reasoning module" (RM). The LM was more or less a "reactive keyboard" for arbitrary 2-level formal languages. The RM started as theorem prover for propositional calculus and used (the topological duals of) Peirce's α graphs as its basic data structure, but soon took a turn toward model-theoretic ways of working when the proof-theoretic pilgrimage sank into a slough of despond.

    It turned out that cacti made a far better data structure than trees for doing all this, so the cactus language for propositional logic grew quite naturally from these seeds.

    Jon
    • CommentRowNumber6.
    • CommentAuthorJonAwbrey
    • CommentTimeSep 13th 2009
    • (edited Sep 15th 2009)

    By the time I got to Chambana (EDITED: was Phoenix) in '84, the LM (code named "Slate") and the RM (code named "Chalk") were pretty well integrated over a common data structure, with the LM and RM applications amounting to different "views" (think "functors") of that datatype. Looking back, I don't know if that was really such a good idea, but it was theoretically interesting to think about lattice operations on datatypes and how to compute the "least common denominator" of several data structures that had initially been tailored to specialized tasks. At any rate, I was pretty much forced to parsimonize everything by the 640K memory bounds that I was working under at the time. Both these programs had been born in a mainframe environment (CyberDyneCystems 6500 @ Michigan State), but some SysAdmin Shogun or other read an article in a magazine saying "AI Is Dead", so they booted our beloved UT-Lisp off the system, and we all had to scramble to build our AI Arks in smaller basements. Common Lisp for PCs was still in its infancy, so I had to translate all my stuff into a succession of Pascals on a series of begged and borrowed clones.

    But I e-gress ...

    • CommentRowNumber7.
    • CommentAuthorJonAwbrey
    • CommentTimeSep 13th 2009
    Another part of my œuvre-all plan was an "isomorphism module" (IM) that had the task of finding isomorphic embeddings of one structure into another. One of the reasons why we need such a thing is, of course, that programming data structures are extremely concrete. To a graph theorist this means "labeled" or "colored" graphs, not abstract graphs. To a logician this means "concretely labeled axioms" (CLA), not "formal axiom schemata" (FAS). Getting the virtues of FAS when all you have to work with is CLA is one of those details that bedevils everything we try to do in symbolic computing. Graph isomorphism is NP-ridiculous, of course, but maybe not for a suitably chosen species of data structures. I never got a chance to develop the IM (code named "Axletree") very far, much less integrate it with the learning and reasoning modules, but I did think I saw what I imagined to be several promising directions.

    Another approach is to eliminate variables entirely and work with something like combinators ...

    Jon

1 to 7 of 7

  1.