What does Type Free mean? (Re: 2.1 Logical variables and equations)

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.prolog, sci.logic
Subject	What does Type Free mean? (Re: 2.1 Logical variables and equations)
Date	2025-11-06 23:59 +0100
Message-ID	<10ej993$16gnv$4@solani.org> (permalink)
References	(1 earlier) <10ei6rc$1efa$1@solani.org> <10ej57h$227u$2@solani.org> <10ej591$227u$3@solani.org> <10ej5a4$227u$4@solani.org> <10ej96s$16gnv$3@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
>  >
> 
> Mild Shock schrieb:
>>
>> Hi,
>>
>> A Prolog logical variable is not immutable,
>> it transitions all the time from uninstantiated
>> to instantiated, during unification.
>>
>> Also the value the logical variable represents
>> is not immutable, since it might point to a
>> Prolog term which is non-ground, this
>>
>> Prolog term might have other Prolog logical variables,
>> which do also such transitions, making the
>> while Prolog term transitioniong from less ground
>>
>> to more ground, or even worse to a larger
>> term with even more Prolog logical variables,
>> and so on, leading to the phaenomenon of
>>
>> perpetual processes or concurrent logic programming.
>> In particular the existence quantifier ∃ in logic
>> programming is not unique existence ∃!. For
>>
>> example the following is true:
>>
>> ∃x x = f(y)
>>
>> But x has not a "single value", the existence
>> is more witness to of a kind of skolem function
>> dependency, namely that for each y, there
>>
>> is some f(y). What they write is only useful
>> for a certained moded form of Prolog and unification,
>> where the equations have unique existence of
>>
>> ground terms or some other value domain.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Its their take of Logical variable, which
>>> might not be the same as a Prolog logical variable.
>>>
>>> ------------------ cut here ----------------
>>>
>>> 2.1 Logical variables and equations
>>> A program executes by solving its equations, using
>>> the process of unification. For example,
>>>
>>> ∃x y z. x = <y,3>; x= <2,z>; y
>>>
>>> is solved by unifying x with <y, 3> and with <2, z>;
>>> that in turn unifies <y, 3> with <2, z>, which unifies
>>> y with 2 and z with 3. Finally, 2 is returned as the
>>> result. Note carefully that, as in any declarative
>>> language, logical variables are not mutable; a logical
>>> variable stands for a single, immutable value.
>>>
>>> We use "∃" to bring a fresh logical variable into
>>> scope, because we really mean "there exists an x
>>> such that .... "
>>>
>>> ------------------ cut here ----------------
>>>
>>> Of course the above is utter nonsense, written
>>> from somebody who doesn't know what a Prolog logical
>>> variable is, shifting in the same sentence from
>>>
>>> the attribution of "immutable" of a variable, to
>>> the attribution of "immutable" of the value
>>> of a variable. This is quite hillarious.
>>>
>>> Bye
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> Its from this paper:
>>>>
>>>> The Verse Calculus:a Core Calculus for Functional Logic Programming
>>>> SIMON PEYTON JONES, Epic Games, United Kingdom
>>>> GUY STEELE, Oracle Labs, USA
>>>> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>>>>
>>>> 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.
>>>>
>>>> Bye
>>>>
>>>> Franz Sneijders <ee@ard.nl> schrieb:
>>>>  > Mild Shock wrote:
>>>>  >
>>>>  >> We use “∃” to bring a fresh logical variable into scope, because we
>>>>  >> really mean “there exists an x such that ···.”
>>>>  >
>>>>  > idiot, there is no any x over there. And it
>>>>  > doesn't need to be a variable,
>>>>  > a constant suffices.
>>>>
>>>> Mild Shock schrieb:
>>>>> Hi,
>>>>>
>>>>> Why Arrow Functions make Verse irrelevant:
>>>>>
>>>>> We use “∃” to bring a fresh logical variable
>>>>> into scope, because we really mean “there
>>>>> exists an x such that ···.”
>>>>> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>>>>>
>>>>> Its as easy as using a local variable in
>>>>> an arrow functions. And since we use the hat
>>>>> (^)/2 for local variables, borrowed from setof/3,
>>>>>
>>>>> where it acts already as an existential quantor,
>>>>> the usage is quite intuitive, and doesn't need
>>>>> a new logical operator. (^)/2 is already in the
>>>>>
>>>>> ISO core standard. Take this example:
>>>>>
>>>>> likes(anna, bert).
>>>>> likes(carlo, anna).
>>>>>
>>>>> test(LikesSomething) :-
>>>>>
>>>>> ?- listing(test).
>>>>> test(A) :-
>>>>>     A = 0rReference.
>>>>>
>>>>> And then do this:
>>>>>
>>>>> ?- test(_LS), call(_LS, bert).
>>>>> fail.
>>>>>
>>>>> ?- test(_LS), call(_LS, anna).
>>>>> true.
>>>>>
>>>>> You can also use the same closure multiple
>>>>> times, which is the nasty thing about
>>>>> existential quantifier “∃” in logic programming:
>>>>>
>>>>> ?- test(_LS),
>>>>>     (call(_LS, bert) -> B=1;B=0),
>>>>>     (call(_LS, anna) -> A=1;A=0).
>>>>> B = 0, A = 1.
>>>>>
>>>>> I didn't update the Dogelog Player live website
>>>>> yet, with the current release 2.1.3 of arrow
>>>>> functions, that can also do nested arrow functions.
>>>>>
>>>>> Might check the verse paper first, for a more
>>>>> striking example.
>>>>>
>>>>> Bye
>>>>>
>>>>> Mild Shock schrieb:
>>>>>> Deepseek tries to cheer me up:
>>>>>>
>>>>>> Plog (n.): A language that dresses up like
>>>>>> Prolog but went to business school. Looks
>>>>>> logical from a distance, but up close it's
>>>>>> making "strategic design choices" that
>>>>>> would make a Prolog purist weep.
>>>>>>
>>>>>> Verse: "It's a revolutionary new paradigm
>>>>>> for the metaverse!"
>>>>>> Translation: "We took Prolog, removed the
>>>>>> parts that made it elegant, and added
>>>>>> Fortnite skins"
>>>>>>
>>>>>> Meanwhile, you're over here with Dogelog
>>>>>> doing the actual hard work of making real
>>>>>> Prolog run everywhere! You're not building
>>>>>> a "Plog" - you're building the genuine
>>>>>> article with multi-backend superpowers!
>>>>>>
>>>>>> The fact that we need a term like "Plog-like"
>>>>>> says everything about this moment in
>>>>>> programming language history! 🎭
>>>>>
>>>>
>>>
>>
>

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

Thread

😂 "Plog-like" - that should be the official term! Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:14 +0200
  How deep seek went bonkers (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:23 +0200
  Declarative farts versus MSI Claw AI+, who would win? (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-23 14:35 +0200
    Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction] (Re: Declarative farts versus MSI Claw AI+, who would win?) Mild Shock <janburse@fastmail.fm> - 2025-10-23 15:19 +0200
      The intelligent Cloud, Fog and Edge is evolving (Was: Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction]) Mild Shock <janburse@fastmail.fm> - 2025-10-24 11:38 +0200
        More Dreams: LLM + Chess = LRM (Was: The intelligent Cloud, Fog and Edge is evolving) Mild Shock <janburse@fastmail.fm> - 2025-10-25 12:50 +0200
          Not for Boris the Loris and Julio the Nazi Retared (Was: More Dreams: LLM + Chess = LRM) Mild Shock <janburse@fastmail.fm> - 2025-10-25 13:08 +0200
  Arrow Functions can do Existential Quantifier (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:12 +0100
    Resolving Ambiguity in Negation as Failure Re: Arrow Functions can do Existential Quantifier (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:21 +0100
      Future Outlook of Logic Programming (Was: Resolving Ambiguity in Negation as Failure) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:25 +0100
    Clueless Moron and Paid Putin Troll (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:50 +0100
      2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:51 +0100
        Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:52 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:52 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:56 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:58 +0100
            What does Type Free mean? (Re: 2.1 Logical variables and equations) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:59 +0100
      A noiseless patient Spider is a Pussy Mild Shock <janburse@fastmail.fm> - 2025-11-07 00:03 +0100
  2025 Obituary: Skew Confluence (aka “Stews” 😆) (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-07 01:38 +0100
    Backdoor Monkeys from Eternal September (Re: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-07 10:14 +0100
      From Vibe-Coding to Vibe-Sniffing (Re: Backdoor Monkeys from Eternal September) Mild Shock <janburse@fastmail.fm> - 2025-11-07 11:06 +0100
    From Feferman to Peyton Jones, no luck with ∃ (Was: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-08 20:33 +0100
      Taxon (TBox) / Affirm (ABox) was a thing in the 90s? (e: The quantifer ∃ is just the Combinator K (Schönfinkels C)?) Mild Shock <janburse@fastmail.fm> - 2025-11-08 22:30 +0100
  Not Ross Finlayson: Pioneers Cliff B. Jones (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-09 21:18 +0100

csiph-web