Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #15120

Write a book about the glorious 1960s (Re: Don't worry, be happy: Take your time)

Show all headers | View raw

Hi,

Philosophy is a mandatory and highly important
subject in the French education system, studied
in the final year of high school (Terminale) and
as part of the Baccalauréat exams.

France has strong philosophy education but weak
interdisciplinary bridges, especially compared
to places like the US, UK, or Germany where
“logic” spans departments.

- Philosophers may focus on conceptual foundations,
argumentation, epistemology.
- Mathematicians/logicians focus on formal systems,
proof theory, model theory.
- Computer scientists focus on algorithms, computation,
complexity, type theory.

But see the positive side. You could write
a book about the glorious 1960s, that saw
the Curry-Howard theorem comming.

- The 1960s counterculture (“hippies”) were
drawn to new ways of thinking: systems, feedback loops, 
interconnectedness — all ideas central to cybernetics.

- Netherlands-based logicians were quietly
inventing AUTOMATH and type theory. probably
visiting a coffee shop from time to time.

Bye

Mild Shock schrieb:
> Hi,
> 
> Don't worry, be happy: Take your time.
> Maybe the matter rings a bell in 1, 2
> or 5 years. Who knows?
> 
> Or even better, in 3, 6 or 12 months.
> Maybe France has somewhere a library
> with a book about Type Theory?
> 
> Or if all else fails try knocking on
> the doors of INRIA, a friendly student
> might appear, and explain the
> 
> matter face 2 face, in a few minutes.
> 
> Bye
> 
> Mild Shock schrieb:
>>
>> "considered consequence". Ha Ha, why this
>> formulation? I voluntarily used the Curry-
>> Howard theorem, when I developed my Prolog
>>
>> code. I didn't invent anything. And its not
>> a smart system. Please never use the word
>> "smart" in software engineering, thats not
>>
>> professional. In particular the Implication
>> Introduction rule has been documented around
>> the world a 100x times: Just have a look:
>>
>> Intuitionistic implicational natural deduction
>>
>> G, A |- B
>> ------------ (->I)
>> G |- A -> B
>>
>> Lambda calculus type assignment rules
>>
>> G, x:A |- t:B
>> ----------------------- (->I)
>> G |- (λx:A.t) : A -> B
>>
>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus 
>>
>>
>> Also refering to the above is probably more
>> useful, than referning to the paper. Since
>> it gives a summary of propositional
>>
>> MINIMAL LOGIC in Curry-Howard simple types.
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Instead presenting a clown world like here:
>>>
>>> - The smart system for printing labels and reference
>>> lines in Fitch proofs has been invented by B., a Prolog
>>> expert who usually dislikes seeing his name quoted.
>>> https://www.vidal-rosset.net/2025-11-17-swi-tinker-for-swi-prolog-provers.html 
>>>
>>>
>>> You could simply state that the Fitch renderer
>>> is derived from Curry-Howard isomorphism proof
>>> terms. This is pretty much folk knowledge in logic
>>>
>>> circles, and wasnt invented by me. I was only
>>> the messenger for things that every Logician should
>>> know, already at least for 60 years, the original
>>>
>>> THE FORMULAE-AS-TYPES NOTION OF CONSTRUCTION
>>> W. A. Howard - University of Chicago
>>> https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf
>>>
>>> Curry-Howard paper already circulated in 1969.
>>> That was around the same time when Automath
>>> ("automating mathematics") was devised by Nicolaas
>>>
>>> Govert de Bruijn, for expressing complete mathematical
>>> theories in such a way that an included automated
>>> proof checker can verify their correctness.
>>>
>>> Bye
>>
>>
> 

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Secret Sauce of Dana Scott and Raymond Smullyan Mild Shock <janburse@fastmail.fm> - 2025-01-18 01:15 +0100
  The Clown World of Joseph Vidal Rosset (Re: Philosophize not God, Philosophize the Door Knob) Mild Shock <janburse@fastmail.fm> - 2025-12-04 11:26 +0100
    The SWI-Prolog community is a circus (Was: The Clown World of Joseph Vidal Rosset) Mild Shock <janburse@fastmail.fm> - 2025-12-04 11:47 +0100
      Alectryon: Long Life Learning or Stable Diffusion? (Was: The SWI-Prolog community is a circus) Mild Shock <janburse@fastmail.fm> - 2025-12-04 13:37 +0100
      From Unrusting Blade to Unburning Icarus (Re: The SWI-Prolog community is a circus ) Mild Shock <janburse@fastmail.fm> - 2026-07-27 12:18 +0200
    "considered consequence". Ha Ha, why this formulation? (Was: The Clown World of Joseph Vidal Rosset) Mild Shock <janburse@fastmail.fm> - 2025-12-04 21:41 +0100
      Don't worry, be happy: Take your time (Re: "considered consequence". Ha Ha, why this formulation?) Mild Shock <janburse@fastmail.fm> - 2025-12-04 21:57 +0100
        Write a book about the glorious 1960s (Re: Don't worry, be happy: Take your time) Mild Shock <janburse@fastmail.fm> - 2025-12-04 22:40 +0100
  Alain Colmerauer: Prologia cirque (Re: Secret Sauce of Dana Scott and Raymond Smullyan) Mild Shock <janburse@fastmail.fm> - 2025-12-04 22:52 +0100
    Where did the "smarts" go? Drinker Paradox fails (Was: Alain Colmerauer: Prologia cirque) Mild Shock <janburse@fastmail.fm> - 2025-12-05 15:46 +0100
      BB(N): Prover should be verified [Henkin Constructive?] (Was: Where did the "smarts" go? Drinker Paradox fails) Mild Shock <janburse@fastmail.fm> - 2025-12-05 16:08 +0100
  The French Square Wheele Bicycle of Logic (Re: Secret Sauce of Dana Scott and Raymond Smullyan) Mild Shock <janburse@fastmail.fm> - 2025-12-05 19:54 +0100
    The episode told everything about the Character (Re: The French Square Wheele Bicycle of Logic) Mild Shock <janburse@fastmail.fm> - 2025-12-05 20:12 +0100

csiph-web