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

Groups > comp.lang.prolog > #15119

Don't worry, be happy: Take your time (Re: "considered consequence". Ha Ha, why this formulation?)

Show all headers | View raw

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