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

Hi,
What I don't know yet, is how to assure that
the context is used affine. Non-affine modus ponens
can be seen as, where E is what is common in both
contexts, and the comma is disjoint union:
    G, E |- A -> B      E, D |- A
   --------------------------------
            G, E, D |- B
In linear logic the linear implication uses
a splitting context:
    G |- A -o B      D |- A
   --------------------------------
            G, D |- B
This is unlike intuitionistic logic, which uses the
Non-affine modus ponense. But the affine modus
ponens uses a splitting context. How implement
proof search efficiently for splitting context?
I have some idea based on DCG. But I didn't find
a paper yet showing such a DCG based search
for linear logic.
Bye
Mild Shock schrieb:

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
>

>