Re: What are Simple Types (Was: Proofs as programs)

Hi,
The typing rules for WE3 are similar to WE2.
The changes are:
- WE2 doesn't require a context
- WE3 requires a context
- WE2 has only modus ponense and constants
- WE3 has additionally deduction theorem and variables
See also here what WE3 requires:
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules
Bye
Mild Shock schrieb:

The requirement for week 3 is explicitly lambda expressions:
 

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.
>
The logic is the same as in Weekend 2.

  For Affine Logic the lambda expressions should have a funny property:
 - A variable occurs only once unbound in the bound scope.
 For example this here, although it has a simple type:
 λ y:A λ x:A->A. x (x y)
 It cannot be a proof term of Affine Logic, since x occurs twice.
 Some testing showed you don't produce lambda expressions:
 You produce:
 

But I am not familiar with this proof display:
>
[
   impI((p->0))
   impI((p->0))
   [
     impE1(1:(p->q))
     impI(p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       botE(3:0)
     ]
   ]
   [
     impE2(1:p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       unif(3:0)
     ]
   ]
]

 Julio Di Egidio schrieb:

On 18/12/2024 15:30, Mild Shock wrote:
>

Maybe your work qualifies for Weekend 3.

>
In fact, I have replied to the WE3 announcement.
>

I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?

>
It implements "affine intuitionistic propositional logic", and I am getting to evaluation/compilation which is the functional side (more details in my initial reply): so, sure, I even classify my reduction rules as intros vs elims...
>
What is the deadline?  I don't know what WE is 3.
>
-Julio
>