Email Gateway (Aug 22 2022 at 19:13): Email Gateway (Aug 22 2022 at 19:13):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
A pedagogical way to express the distinction between simple type theory and
dependent type theory is as follows.
Roughly speaking, a type theory is a simple type theory iff types are not
parameterized, e.g., the type of matrices is not parametrized by the
dimensions of the matrices. In order to specify the dimension of a given
matrix, a function should be defined.
Roughly speaking, a type theory is a dependent type theory iff types can be
parametrized, e.g., the type of matrices can be parametrized by the
dimension of the matrices.
In order to translate dependent type theory to simply type theory, a good
strategy is to define some function playing the role of the parameters.
Kind Regards,
José M.
El vie., 22 feb. 2019 a las 12:39, Freek Wiedijk (<freek@cs.ru.nl>)
escribió:
Email Gateway (Aug 22 2022 at 19:14):From: Freek Wiedijk <freek@cs.ru.nl>
Dear José,
A pedagogical way to express the distinction between simple
type theory and dependent type theory is as follows.
[...]
I strongly disagree. In the Mizar system one has "dependent
types" exactly in the way that you describe it. But Mizar
is in no way based on "dependent type theory". It does
not have typed lamdba terms in _any_ fashion, so it is
certainly not based on "type theory". It _does_ have types,
and the types are parametrized exactly like you describe it.
Which means it has dependent types. But is not based on
type theory, let alone on dependent type theory.
My "pedagogical way" would be to say that in dependent type
theory, one has typed lamdba terms represent the proofs.
I.e., it is based on the Curry-Howard isomorphism.
So:
simple type theory
typed lambda terms for terms/formulas
no lambda terms for proofs
dependent type theory
typed lambda terms for terms/formulas/proofs
Dependent type theory really is the grand unification of
formal stuff: _everything_ is a typed lambda term there!
Whether this is a good thing is disputable. It naturally
leads to constructive logic, which is a distraction if
you want to formalize classical mathematics. Which is my
main interest.
Freek
Email Gateway (Aug 22 2022 at 19:14):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
According to nlab:
any type theory is called a simple type theory if type formation is not
https://ncatlab.org/nlab/show/simple+type+theory
Do you agree with this definition?
Last updated: Apr 24 2024 at 20:16 UTC