gusl: (Default)
[personal profile] gusl
Alessio Guglielmi
...
My second research objective is to come up with useful, interesting notions of identity of proofs. It is embarrassing for proof theory that the natural question of `when are two proofs to be considered identical?ยด lacks good answers.* (This question is tightly connected to the equally non-well-understood problem of deciding when two algorithms are the same.) One reason for our embarrassment is that the notion of normalisation available, viz. cut elimination, is inadequate to decide the question; I believe that the problem is that this is the only (reasonable) normalisation notion available in the sequent calculus and natural deduction. Thanks to its finer granularity, the calculus of structures offers several natural new notions of normalisation, this way improving our ability to study new concepts of identity.
...


Finally someone addresses my question about proof uniqueness! Google wasn't helping me at all, so I had to find it by accident.



Dan Sperber researches language, cognition, culture and evolution
(will be screened)
(will be screened if not validated)
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

February 2020

S M T W T F S
      1
2345678
9101112131415
16171819202122
23242526272829

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags