Formality. Новый язык зависимых типов
От: HrorH  
Дата: 15.09.19 12:50
Оценка: 23 (2)
Formality (см там внизу страницы мультик)


Что интересного:
Solving the mystery behind Abstract Algorithm’s magical optimizations

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

Towards a simple theorem prover

Can we call a function a googol times?

Своя операционная система Moonad

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, Self types, SYMMETRIC INTERACTION COMBINATORS, Магия, Cedille, Juvix

P.S. Похоже про interaction net лучше сначала прочитать статью interaction net Lafont
потом Yves Lafont, Interation Combinators, Institut de Mathematiques de Luminy, 1997
и потом A Denotational Semantics for the Symmetric Interaction Combinators Mazza
Отредактировано 23.09.2019 11:31 HrorH . Предыдущая версия . Еще …
Отредактировано 15.09.2019 20:29 HrorH . Предыдущая версия .
Отредактировано 15.09.2019 18:56 HrorH . Предыдущая версия .
Re: Источник
От: Qbit86 Кипр
Дата: 15.09.19 21:23
Здравствуйте, HrorH, Вы писали:

HH>Formality. Новый язык зависимых типов

Откуда ты про него услышал?
Глаза у меня добрые, но рубашка — смирительная!
Re[2]: Источник
От: HrorH  
Дата: 15.09.19 21:28
Оценка: 1 (1)
Здравствуйте, Qbit86, Вы писали:

Q>Откуда ты про него услышал?

Случайно нагуглил Juvix: dependent-linearly-typed core language with optimal reduction and interaction nets

Formality has been a major inspiration. The interaction net rules in Juvix are closer to those in this paper but I doubt we would have found out about the literature without Victor's fantastic blog posts.

Подождите ...
Пока на собственное сообщение не было ответов, его можно удалить.