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


Groups > sci.physics.relativity > #667136

Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll)

From Mild Shock <janburse@fastmail.fm>
Newsgroups sci.physics.relativity, sci.math
Subject Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll)
Date 2025-11-06 22:42 +0100
Message-ID <10ej4p1$21va$1@solani.org> (permalink)
References <10c46uv$mf1d$3@solani.org> <10ei81g$1f1r$5@solani.org> <10eimpq$19gek$2@dont-email.me> <10ej3uh$21i5$1@solani.org> <10ej4au$21re$1@solani.org>

Cross-posted to 2 groups.

Show all headers | View raw


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 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.
>>>
>>
> 

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