[FOM] Wiki: type theoretic fnds
Patrik Eklund
peklund at cs.umu.se
Thu Mar 31 01:14:55 EDT 2016
Harvey,
Here is a simple reason why category theory can be supportive.
If you look at classical terms, we say "Constants and variables are
terms, and if omega is an operator with t1,...,tn as terms, then
omega(t1,...,tn) is also a terms. These are the only terms."
This definition can be formalized to appear as a term monad, but it adds
nothing as such, many say. However it adds in applications, since with
that underlying term functor we can compose with other functors, and
also view the functor over other categories than just the category of
sets.
For "lambda terms" the situation is different. Traditionally we say
"Variables are \-terms. If M is a \-term, then so is \x.M. If MN are
\-terms, then so is MN.". This is seens as an "elegant" definition by
computer scientists, even if they at the same time acknowledge, that the
definition brings in undesirable \-terms. Tricks are needed to fix it.
Here is where Church again comes into play. Church said that '\' is an
informal symbol, and we have formalized the construction of \-terms so
that '\' is not an "abstractor" of operators or terms, but the operator
itself takes care of its own abstraction. Some detail you see in the
paper
http://www.glioc.com/files_glioc/ModernEyesOnLambdaCalculus.pdf
and attached also our Fuzzy Terms paper with the formal and categorical
term construction in both cases.
As one example we show how the informal treatment of "description logic"
(the logic in web ontology, Google) can be formalized, and indeed
extended with composition and being over other categories, which opens
up perspectives for applications.
Curry and Howard were always cautious about these things since they knew
something was fishy, but apparently they could never put their fingers
on it. Martin-Löf showed no scruples and simply started to "reformalize
foundations" with similarly sloppy symbolism. Computer scientists and
secondhand logicians followed him like bankvoles. Today if you hear HoTT
fanatics explain their content, you will not understand it, because even
they don't. There is simply nothing to understand. As I often say, if
something in their theory becomes questionable, they bring in stuff from
the outside, so as to say.
You could also say that their approach hides things, and this makes it
very hard to analyze. A bit like Turing machines. Recursion is hidden
and never really brought up front. This is the reason why the
Church-Turing thesis remains a mystery, since Church-Kleene-Gödel keeps
all of recursion within the machinery, where Turing's approach hides it
an it becomes "algorithm".
To conclude, type theory stays deliberately informal, and they can
therefore continue to attract "algorithm" believers. But for
foundations, it's no good. Similarly, I am concerned with set theory as
being untyped, and quantifier symbols being similarly informal as
compared to the lambda symbol. The FOM community is also stubborn, and
this is the reasoin why I am a bit allergic against "wisdom".
There is no moderation of these things, and very few think in these
directions. For us it is not just important formalization, but it helps
us develop more elaborate applications, e.g. in conerning logic as
potentially to be used in health care. Evidence-based medicine is awful.
We need logic-based medicine.
And so on and so forth.
Sorry for spamming you, but your mail correlates with some thoughts I
tried to present last year, but my postings were indeed rejected. I am
therefore happy to continue to read your postings, as I have been also
in the past, even if not replying to them earlier.
Similar type theory debates have taken place under the categories
mailing list, where my postings have been accepted. I have been openly
very critical against the type theory communities. Some understand, but
the categorical machinery is quite heavy, so those not well versed in
it, will reject it.
Best,
Patrik
On 2016-03-30 23:20, Harvey Friedman wrote:
> I looked some at
>
> https://en.wikipedia.org/wiki/Univalent_foundations
>
> https://en.wikipedia.org/wiki/Homotopy_type_theory
>
> As I expected, I could not find a single example of any of the
> following:
>
> 1. Some issue in f.o.m. that is not being addressed by the usual f.o.m.
> 2. Some issue in f.o.m. that is being addressed by type theoretic
> f.o.m.
>
> I see some new algebraic/topological type interpretations of type
> theories, and the like.
>
> Although it wasn't clear from these articles, I could imagine that
> there is some kinds of type theories for which it is not at all
> obvious that one has any mathematical model, or even that one has any
> model at all in any reasonable sense.
>
> So the impression one inevitably gets is that this stuff is
>
> a. A framework for doing some new kinds of abstract categorical
> algebra/topology that is exciting to very abstractly minded
> mathematicians.
> b. A complicated solution in search of a foundational problem.
>
> So I repeat my suspicion and therefore my challenge.
>
> Anything that can be done with this kind of "foundations" can be done
> much more simply and much more powerfully and much more effectively by
> sugaring the usual f.o.m.
>
> But I can't start backing this up, and others cannot really challenge
> me, until they state a crystal clear foundational issue that they
> think is not or cannot be addressed in standard f.o.m., and that is
> addressed in this exotic f.o.m.
>
> One thing that does not seem to be in doubt, correct me if I am wrong.
> This exotic f.o.m. is much more complicated than standard f.o.m.
>
> Perhaps we should start with a simpler question.
>
> What foundational issue is addressed by even ML type theory - no
> univalence axiom - that cannot be more simply and better addressed by
> standard f.o.m.?
>
> Let me close with a methodological question.
>
> What standards should be applied by proposing to replace an existing
> system with another system that is massively more complicated?
>
> My answer of course as you see, is to ask for careful generally
> understandable explanations as to what is to be gained. There also
> needs to be a major effort made to see if the existing much simpler
> system already can be used to address the issues, whatever they are,
> adequately, or maybe even better.
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Fuzzy Terms reprint.pdf
Type: application/pdf
Size: 494260 bytes
Desc: not available
URL: </pipermail/fom/attachments/20160331/14c6ce2c/attachment-0001.pdf>
More information about the FOM
mailing list