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


Groups > sci.physics.relativity > #667142

What does Type Free mean? (Was: Clueless Moron and Paid Putin Troll)

From Mild Shock <janburse@fastmail.fm>
Newsgroups sci.physics.relativity, sci.math
Subject What does Type Free mean? (Was: Clueless Moron and Paid Putin Troll)
Date 2025-11-06 23:54 +0100
Message-ID <10ej8uo$16gnv$1@solani.org> (permalink)
References (1 earlier) <10ei81g$1f1r$5@solani.org> <10eimpq$19gek$2@dont-email.me> <10ej3uh$21i5$1@solani.org> <10ej6m5$1eobm$1@dont-email.me> <10ej8fl$16gd8$1@solani.org>

Cross-posted to 2 groups.

Show all headers | View raw


Hi,

I was crediting these guys for arrow functions:

 > Hiord: A Type-Free Higher-Order Logic Programming
 > Language with Predicate Abstraction
 > Daniel Cabeza, Manuel V. Hermenegildo, Manuel V. Hermenegildo
 > https://www.researchgate.net/publication/221052995

What does Type Free mean? It basically
means no bounded quantifiers like in ∃x ∈N.
No restriction per se to natural numbers or

something. Only universal algebra respectively its
incarnation via Herbrand Domains. Did you
see a bounded quantifer of the form ∃x ∈D where

D is some domain in the verse example? I only
see ∃x without the ∈D. What values where they
talking about? I mean they had numbers 3, 2, and

then they had what? Also pairs via <_,_>.

Bye

P.S.: Need help with what a bounded quantifer is:

https://en.wikipedia.org/wiki/Bounded_quantifier


Mild Shock schrieb:
> Hi,
> 
> Please read the verse paper and the
> type free hiord paper, to have have
> slightest clue what the context is.
> 
> Bye
> 
> Mariano Amelsvoort schrieb:
>> Mild Shock wrote:
>>
>>> Don't blame me for what they write.
>>> But mostlikely your eruption is just from a clueless Nazi Retard, namely
>>> the paid
>>>
>>> troll you are, getting money from Putin.
>>
>> here is a one with a constant, admit you don't know what you say and what
>> you do
>>
>>   ∃x ∈N: x×x=36
>>
> 

Back to sci.physics.relativity | Previous | NextPrevious in thread | Next in thread | Find similar | Unroll thread


Thread

Re: Arrow Functions can do Existential Quantifier (Re: 😂 "Plog-like" - that should be the official term!) Franz Sneijders <ee@ard.nl> - 2025-11-06 17:44 +0000
  Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:28 +0100
    2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:35 +0100
      Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:42 +0100
        Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:48 +0100
    Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mariano Amelsvoort <aa@viollr.nl> - 2025-11-06 22:15 +0000
      Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:46 +0100
        What does Type Free mean? (Was: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:54 +0100
  A noiseless patient Spider is a Pussy Mild Shock <janburse@fastmail.fm> - 2025-11-07 00:03 +0100
    Re: A noiseless patient Spider is a Pussy Jackie Romijnders <jirke@jecjr.nl> - 2025-11-07 00:01 +0000
  2025 Obituary: Skew Confluence (aka “Stews” 😆) (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-07 01:42 +0100
    The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃) Mild Shock <janburse@fastmail.fm> - 2025-11-08 21:27 +0100
      Re: The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃) Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-08 18:20 -0800
        Horn uses Conditional / Clark uses Biconditional (Was: The quantifer ∃ is just the Combinator K (Schönfinkels C)?) Mild Shock <janburse@fastmail.fm> - 2025-11-09 13:05 +0100
          CET is also needed (Was: Horn uses Conditional / Clark uses Biconditional) Mild Shock <janburse@fastmail.fm> - 2025-11-09 13:08 +0100
            Re: CET is also needed (Was: Horn uses Conditional / Clark uses Biconditional) Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-09 08:13 -0800
              You have to check Feferman OST [Paradox Hunting] (Was: CET is also needed) Mild Shock <janburse@fastmail.fm> - 2025-11-09 19:57 +0100
                Prolog semantics is 3-valued or intuitionistic [Feferman prefers partial logic] (Was: You have to check Feferman OST [Paradox Hunting]) Mild Shock <janburse@fastmail.fm> - 2025-11-09 20:11 +0100
                In Prolog you don't need the down arrow t↓ (Was: Prolog semantics is 3-valued or intuitionistic) Mild Shock <janburse@fastmail.fm> - 2025-11-09 20:16 +0100

csiph-web