هندسة التفاعل

في نظرية البرهان ، قدّم جان إيف جيرار هندسة التفاعل (GoI) بعد فترة وجيزة من عمله على المنطق الخطي . في المنطق الخطي، يمكن النظر إلى البراهين على أنها أنواع مختلفة من الشبكات، على عكس هياكل الشجرة المسطحة في حساب المتتاليات . ولتمييز شبكات البرهان الحقيقية عن جميع الشبكات الممكنة، وضع جيرار معيارًا يتضمن مسارات في الشبكة. يمكن اعتبار المسارات في الواقع نوعًا من المؤثرات التي تؤثر على البرهان. انطلاقًا من هذه الملاحظة، وصف جيرار ^{[ 1 ]} هذا المؤثر مباشرةً من البرهان، وقدّم صيغة، تُعرف بصيغة التنفيذ ، تُشفّر عملية إزالة القطع على مستوى المؤثرات. اقترح جيرار في أعماله اللاحقة نماذجًا تُمثّل فيها البراهين على شكل تدفقات، ^{[ 2 ]} أو مؤثرات في جبر فون نيومان . ^{[ 3 ]} عُمّمت هذه النماذج لاحقًا بواسطة نماذج رسوم التفاعل لسيلر . ^{[ 4 ]}

كان من أوائل التطبيقات المهمة لنظرية الألعاب (GoI) تحليلٌ أفضل ^{[ 5 ]} لخوارزمية لامبينغ ^{[ 6 ]} لتحقيق الاختزال الأمثل لحساب لامدا . وقد كان لنظرية الألعاب تأثيرٌ كبير على دلالات الألعاب في المنطق الخطي و PCF .

إلى جانب التفسير الديناميكي للبراهين، توفر هندسة بنى التفاعل نماذج للمنطق الخطي ، أو أجزاء منه. وقد درس سيلر ^{[ 7 ]} هذا الجانب باستفاضة تحت مسمى التحقق الخطي، وهو شكل من أشكال التحقق يأخذ في الحسبان الخطية.

تم تطبيق GoI على تحسين المترجمات العميقة لحسابات لامدا . ^{[ 8 ]} وقد استُخدم إصدار محدود من GoI يُطلق عليه اسم هندسة التركيب لتجميع لغات البرمجة عالية الرتبة مباشرةً في دوائر ثابتة. ^{[ 9 ]}

• تم تقديم درس تعليمي حول نظرية الذكاء الاصطناعي في سيينا 07 من قبل لوران رينييه، في ورشة عمل المنطق الخطي.
• هندسة التفاعل في مختبر n