Path: ...!weretis.net!feeder9.news.weretis.net!news.quux.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic,comp.lang.prolog
Subject: Re: Chicken and egg, with curry?
Followup-To: comp.lang.prolog
Date: Fri, 3 Jan 2025 21:37:28 +0100
Organization: A noiseless patient Spider
Lines: 41
Message-ID: <vl9hq8$3ui38$2@dont-email.me>
References: <vl9fs3$3ui38$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 03 Jan 2025 21:37:29 +0100 (CET)
Injection-Info: dont-email.me; posting-host="45659d747365cbcc574a369aa42157b1";
	logging-data="4147304"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18xSMQuFgxeOV8zdCfwgBBRJve61UO9qM8="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:fZo+vp5I+Z1mMI+APEdVwWixPxY=
In-Reply-To: <vl9fs3$3ui38$1@dont-email.me>
Content-Language: en-GB
Bytes: 2726

On 03/01/2025 21:04, Julio Di Egidio wrote:
> Partial and tentative:
> 
> ```
>    Functional = Closures/applications, Reduction/canonicity
>      /    |
> Logical  |   = Predicates/queries, Resolution/subsumption
>      \    |
>    Imperative = Procedures/invocations, Execution/...
> ```
> 
> And there are two views of that triangle: Logical is the top of the 
> *ideal* such triangle, along the lines of a universe with Prop on top, 
> which we can reason with; Imperative is the bottom of a *concrete* such 
> triangle, the bootstrap as well as the final point of application of any 
> concrete system.
> 
> And Logical is the constructive (structural) type-theory founding the 
> Functional, where Functional exists for expressivity and modularity 
> (what else?), plus can be compiled back/down to machine language...
> 
> Right?

BTW, there are deficiencies of standard Prolog that are indeed very 
annoying, to the point that some invoke for the other way round:

HANSEI / Re-thinking Prolog
<https://okmij.org/ftp/kakuritu/logic-programming.html#vs-prolog>

But, besides that I would not put logic in terms of "guessing", I'd 
propose we just need a Prolog that doesn't have the self-inflicted 
quirks: a strengthened resolution with declarative determinism and 
indexing, and a strengthened semantics, of variables and/vs open terms, 
with a partial order of terms by subsumption, and unifiability as 
comparability (a purely structural type system definitionally), i.e. 
where a variable is the most general term...  Or something like that.

No?

-Julio