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

Well you wrote:
 > > It cannot be a proof term of Affine Logic, since x occurs twice.
 > That is not what affine logic means.
It exactly means that. Contraction means occurs twice.
For example this combinator W does not exist in affine
logic. It has the below type, so it shows left Contraction,
the two A are contracted into a single A:
W: ((A -> (A ->B)) -> (A -> B))
As a lambda expression it has a variable that occurs twice:
W = λxλy.((x y) y)
"The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry (1930)."
https://en.wikipedia.org/wiki/B,_C,_K,_W_system
Affine logic has a calculus which is Currys calculus minus
the W combinator and the K combinator replaced by the I combinator.
Julio Di Egidio schrieb:

On 19/12/2024 02:37, Mild Shock wrote:
<https://en.wikipedia.org/wiki/Affine_logic>
<https://en.wikipedia.org/wiki/Substructural_type_system>