Информация об изменениях

Сообщение Formality. Новый язык зависимых типов от 15.09.2019 12:50

Изменено 15.09.2019 18:56 HrorH

Formality. Новый язык зависимых типов
Formality (см там внизу страницы мультик)

Документация

Что интересного:
Functions may behave as if they had negative complexity on optimal evaluators

Своя версия лямбда исчисления

Towards a simple theorem prover

Can we call a function a googol times?

Okay, nobody reads my Twitter, so I realized I can make random, misguided predictions here and nobody will call me dumb if they don't work out, yet I can tell everyone I was right if they do!

So, here is one: there are many similarities between applying quantum operators to multiple values, and performing computations on highly shared terms of interaction combinators. Conjecture: interaction nets can perform Shor's Algorithm efficiently in classical computers.

Victor Maia

Теги: Affine logic, SYMMETRIC INTERACTION COMBINATORS, Магия, Cedille, Juvix
Formality. Новый язык зависимых типов
Formality (см там внизу страницы мультик)

Документация

Что интересного:
Functions may behave as if they had negative complexity on optimal evaluators

Своя версия лямбда исчисления

Towards a simple theorem prover

Can we call a function a googol times?

Okay, nobody reads my Twitter, so I realized I can make random, misguided predictions here and nobody will call me dumb if they don't work out, yet I can tell everyone I was right if they do!

So, here is one: there are many similarities between applying quantum operators to multiple values, and performing computations on highly shared terms of interaction combinators. Conjecture: interaction nets can perform Shor's Algorithm efficiently in classical computers.

Victor Maia

Теги: Affine logic, SYMMETRIC INTERACTION COMBINATORS, Магия, Cedille, Juvix

P.S. Похоже про interaction net лучше сначала прочитать статью interaction net Lafont и потом OBSERVATIONAL EQUIVALENCE AND FULL ABSTRACTION IN THE SYMMETRIC INTERACTION COMBINATORS DAMIANO MAZZA