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: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)
Date: Thu, 19 Dec 2024 18:40:47 +0100
Organization: A noiseless patient Spider
Lines: 64
Message-ID: <vk1lqu$2s7tr$1@dont-email.me>
References: <vjks2t$sghb$1@solani.org> <vjksaq$sgo6$1@solani.org>
 <vjksdb$sgo6$2@solani.org> <vjs63g$1m603$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 19 Dec 2024 18:40:47 +0100 (CET)
Injection-Info: dont-email.me; posting-host="5c82a02c1e2f107e6a78dfd6f7615e23";
	logging-data="3022779"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+feVGjTrQsEQOiDx6aEHla8UDpyG7Mcj4="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:COBdF3z/tJkkC4qarJqyj2QlAP8=
In-Reply-To: <vjs63g$1m603$1@dont-email.me>
Content-Language: en-GB
Bytes: 2678

On 17/12/2024 16:41, Julio Di Egidio wrote:
> On 14/12/2024 22:13, Mild Shock wrote:
> 
>> Create a proof search in Simple Types,
>> that finds Lambda Expressions as proof,
>> for a given formula in propositional logic.
> 
> Thinking about it:
> 
> Either by hand or with a 'solve', we/I [*] go from a Goal to a Proof 
> (proof tree).  And, by Curry-Howard, that is (already!) our Type and 
> witnessing Term, i.e. our Proof is a program whose type is the Goal. 
> Indeed, we also already find type-checking: of a Proof against the Goal 
> it alleges to be a proof of.
<snip>

My interpretation might be unorthodox, anyway here is concretely what I 
am doing (a far better approximation that is): 
<https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>

So yeah, my system definitely qualifies, assuming I meet a deadline that 
remains a mystery to this point - I guess that's the main challenge.

> <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-pl>

Meanwhile, kindly, for your records:

```
?- case(codile, LT, G), prove(LT, G, Ps), print_ps(Ps).  % v30-alpha
[
   orE(0)
   [
     orIL
     impE(2)
     [
       init(0)
     ]
     [
       init(0)
     ]
   ]
   [
     orIR
     impE(1)
     [
       init(0)
     ]
     [
       init(0)
     ]
   ]
]
LT = pos,
G = ([(p->q),(r->s),p\/r]=>q\/s),
Ps = [orE(0),[orIL,impE(2),[init(0)],[init(0)]],
       [orIR,impE(1),[init(0)],[init(0)]]] .

% 3 more solutions...
```

Have fun,

-Julio