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: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)
Date: Tue, 17 Dec 2024 16:41:35 +0100
Organization: A noiseless patient Spider
Lines: 36
Message-ID: <vjs63g$1m603$1@dont-email.me>
References: <vjks2t$sghb$1@solani.org> <vjksaq$sgo6$1@solani.org>
 <vjksdb$sgo6$2@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 17 Dec 2024 16:41:36 +0100 (CET)
Injection-Info: dont-email.me; posting-host="0aa295d1c2f76c0580c40292d69f24bd";
	logging-data="1775619"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+K6onOfrdbYB5LLtiHhlT+0Zc+uoi5v+M="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:GceJ8gEUtxP8evpnnxLqpKIrIwk=
In-Reply-To: <vjksdb$sgo6$2@solani.org>
Content-Language: en-GB
Bytes: 2546

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.

What program does the Proof represent?  If a Goal is of the form `G=>Z`, 
where `G` is the context (some collection of Formulas as hypotheses), 
and Formula `Z` is the conclusion, we interpret a Goal as a function 
from the hypotheses to the conclusion.

To execute a Proof we need a "machine", namely, a function 'eval' that 
takes the Proof as well as witnessing Terms for each hypothesis, and 
returns a Term witnessing the conclusion.  (Which also requires a system 
of Terms: but I am not yet sure about the details...)

More than that, we can 'compile' the Proof to some target language (the 
system's host language being the first candidate), to produce a function 
in the target language that is like 'eval' except specialized to the 
given Proof as well as to as many hypothesis Terms as can be fixed...

Sounds good?  Anything else?  :)

-Julio

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