Deutsch   English   Français   Italiano  
<vl9fs3$3ui38$1@dont-email.me>

View for Bookmarking (what is this?)
Look up another Usenet article

Path: ...!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
Subject: Chicken and egg, with curry?
Date: Fri, 3 Jan 2025 21:04:19 +0100
Organization: A noiseless patient Spider
Lines: 23
Message-ID: <vl9fs3$3ui38$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 03 Jan 2025 21:04:19 +0100 (CET)
Injection-Info: dont-email.me; posting-host="45659d747365cbcc574a369aa42157b1";
	logging-data="4147304"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18/lG+5Iiy2x3/2na2zRUm1TYBVXchw5CQ="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:vKI0mxAS3S0ZOKAhUZLHyP2Q6Zw=
Content-Language: en-GB
Bytes: 1691

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?

-Julio