Ішінара реттелген логика үшін тиімді белгілерді қалай жасау керек?

Мен ресурстық шектеулі ортадағы бағдарламалар туралы ойлау үшін логиканы дамытамын. Менің бастапқы нүкте - интуициялық сызықтық логика, бірақ мен келесі өзгерістер жасадым:

  1. In intuitionistic linear logic, environments are sets of available resources. In my logic, environments are partially ordered sets: some resources have to be consumed before others.

    • Multiplicative conjunction splits into two connectives: parallel conjunction and sequential conjunction.

    • Linear implication can only consume a resource X, if there is no other resource Y that must be consumed before X.

  2. Logical connectives are usually defined in terms of introduction and elimination rules. In my logic, I need a new kind of rule: usage rules, which describe how a resource can be used in a computation without destroying it.

    • I add a new unary operator, called borrowed pointer, which denotes a non-owning reference to an existing resource.

    • Creating a borrowed pointer uses but does not consume the resource being pointed. In particular, one may always create a borrowed pointer to an existing resource X, even if there is some resource Y that must be consumed before X.

    • No resource may be consumed until all borrowed pointers to it have been consumed. This is my main motivation for introducing the notion of sequential conjunction in the first place.

Мен осы логиканың табиғи шегерімін және дәйекті есептеуді қолданып, ережелерін ресми түрде ұсынуды қалаймын. Дегенмен, идеяларды қысқаша баяндайтын жақсы нотациямен келу қиынға соғады:

  1. $ \ Gamma $ ортасы $ \ Delta, \ Sigma $, $ \ Delta $ кез келген ресурс алдында тұтынылатын $ \ Sigma $ -да ресурс болмаған шағын орталарға бөлінуі мүмкін.

  2. $ Gamma $ және $ A \ in \ Gamma $ ресурсын ескере отырып, $ {\ rm ref} $ $ -ға $ Gamma $ ресурсын қосудың нәтижесі $ {$ Rm ref} A $ $ A $ алдында жұмсалуы керек.

  3. $ A $ және $ B $ қатардағы байланысы.

  4. және т.б.

Бұл логика үшін жақсы белгілерді жобалау үшін қандай нұсқауларды ұстануым керек?

3
Жақсы презентация туралы абсолютті түсінік жоқ. Мұның бәрі онымен не істегіңіз келетініне байланысты. Мета-теореманы қысқартылған жою сияқты дәлелдеу үшін дәйекті стиль ұсыну мүмкін. Нақты шағымдар үшін табиғи шегерім дұрысырақ болуы мүмкін. Etc.
қосылды автор PKG, көзі
Теру жүйелері көбінесе табиғи шегерім стилінде ұсынылған логика ретінде оңай көрінеді.
қосылды автор PKG, көзі
@MartinBerger: Соңғы мақсат - бұл логиканы жүйелік бағдарламалау үшін функционалдық тілдің типі үшін негіз ретінде пайдалану.
қосылды автор marko, көзі
@DamianoMazza: рахмет, мен қараймын.
қосылды автор marko, көзі
Мультипликативтік noncommutative логика бойынша Abrusci және Ruet шабыт болуы мүмкін бе?
қосылды автор david6, көзі

Жауап жоқ

0