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

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

Some testing showed you don't produce lambda expressions:

A proof tree is not a lambda expression.

You produce:

I produced: a month has passed and I am at version 30.

But I am not familiar with this proof display:

From: Mild Shock <janburse@fastmail.fm>
Date: Mon, 18 Nov 2024 23:22:11 +0100
Subject: Re: How to prove this theorem with intuitionistic natural deduction?
 > 0: P -> (Q -> R) (Premisse)
 > 1: P /\ Q        (Assumption)
 > 2: P             (/\E,1)
 > 3: Q -> R        (->E,0,2)
 > 4: Q             (/\E,1)
 > 5: R             (->E,3,4)
 > 6: P /\ Q -> R   (Discharge,1)
Confront with this one:
?- prove([p->q->r]=>p/\q->r, Ps), print_ps(Ps).
[
   impI
   andE(0)
   impE(2)
   [
     init(1)
   ]
   [
     impE(0)
     [
       init(0)
     ]
     [
       init(0)
     ]
   ]
]
Modulo finer technical details, it's the same.

What is the deadline?  I don't know what WE is 3.

You haven't answered that one.
-Julio