Teşekkürler @EliBenSasson!

"İnsanlar hangi dillerde programlayacaktır."

Bildiğiniz gibi polinom devreleri *doğrulamak* için kullanılır. Cairo bu ayrımı gizlemek için belirli bir programlama metaforunu (Cairo VM) kullanıcıya sunmak amacıyla kullanır, bu iyidir, ancak her durumda önemli olan kodlanmış şey değil, doğrulanmış olan şeydir.

Örneğin: fonksiyonlar doğrudan (birinci derece) mantıkta belirtilebilir. Makalenin 3. bölümü bunun nasıl yapıldığını gösterir ve özellikle Gabbay'ın çerçevesinde genel tekrar eden fonksiyonlar da dahil olmak üzere bir dizi fonksiyon sunar. Makalede yazıldığı şekliyle bu, teorisyenlere yönelik teorik bir tanımdır ve buna göre Gabbay sonlu alanlar yerine rasyoneller kullanır -- ancak benzer ilkelerin sonlu bir alan üzerinde de geçerli olacağı oldukça açıktır. Bu önemli bir ayrım değildir.

Özel bir durum ilgilidir: Gabbay'ın makalesinden açıktır ki türev ağaçlarının geçerliliği bu çerçevede belirlenabilir - örneğin SK kombinasyonu indirimin için türev ağaçlarının belirlenmesi, kendi başına ilginçtir ve diğer birçok tanım için paradigmatiktir. Eğer bir programlama soyutlaması sunmak istiyorsak, bu, minimum üst geçit içeren, matematiksel açıdan doğru bir yoldur. Başkaları da vardır.

Yukarıdakiler matematiksel bir kanıt olmasa da, umarım bu sorunun bir örneğini vermektedir.