Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: Happy Now? (Was: Please be patient)
Date: Fri, 20 Dec 2024 19:49:46 +0100
Organization: A noiseless patient Spider
Lines: 47
Message-ID: <vk4e8a$3f87m$3@dont-email.me>
References: <vjks2t$sghb$1@solani.org> <vk2i2c$1gvoe$1@solani.org>
 <vk2ie7$1h00a$1@solani.org> <vk49vq$3f87m$1@dont-email.me>
 <vk4ah4$14gh0$1@solani.org> <vk4bi2$3f87m$2@dont-email.me>
 <vk4cd3$1i15s$1@solani.org> <vk4d67$1i1iv$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 20 Dec 2024 19:49:47 +0100 (CET)
Injection-Info: dont-email.me; posting-host="9738968354f61e8f4df4d420c93f95f0";
	logging-data="3645686"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19/R1jlFxlPy5BcMzfEE5YCX+iN90CA4fc="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:P1kmgRSkZDPyH/QtAWiUfNJVbu0=
In-Reply-To: <vk4d67$1i1iv$1@solani.org>
Content-Language: en-GB
Bytes: 2280

On 20/12/2024 19:31, Mild Shock wrote:

> <https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p>
> 
> /* 3 positive test cases */
> 
> % ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
> % N = 3,
> % X = c*k .
> 
> % ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
> % N = 7,
> % X = c*(c*k*k) .
> 
> % ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
> % N = 1,
> % X = k .
> 
> /* 2 negative test case */
> 
> % ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
> % false.

Hmm, gentzen proves them all:

```
?- prove(pos, []=>(a->a)->(a->a), Ps).
Ps = [impI,init(0)] ;
Ps = [impI,impI,init(0)] ;
Ps = [impI,impI,impE(1),[init(0)],[init(0)]] ;
false.

?- prove(pos, []=>a->((a->b)->b), Ps).
Ps = [impI,impI,impE(0),[init(0)],[init(0)]] ;
false.

?- prove(pos, []=>a->(b->a), Ps).
Ps = [impI,impI,init(1)] ;
false.

?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
false.
```

-Julio