Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan https://www.youtube.com/watch?v=omz6SbUpFQ8
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
On 08/01/2025 01:10, Mild Shock wrote:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
Define Smullyan.
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`. Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
F (T -> U) False (F T U).
```
-Julio
Julio Di Egidio schrieb:
On 08/01/2025 01:10, Mild Shock wrote:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
Define Smullyan.
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`. Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
F (T -> U) False (F T U).
```
Thats System F and not simple types. also
known as the polymorphic lambda-calculus
or second-order lambda-calculus, it is an
extension of simply typed lambda-calculus.
But in simple types itself, th self application
x x has no type. You can try yourself:
/* Typed Variable */
typeof(_:A, B) :-
unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
And then the query:
?- X=_:_, typeof((X*X), T).
false.
The query will though succeed if you remove
the occurs check.
On 08/01/2025 10:31, Mild Shock wrote:
Julio Di Egidio schrieb:
On 08/01/2025 01:10, Mild Shock wrote:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
Define Smullyan.
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`. Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
F (T -> U) False (F T U).
```
Thats System F and not simple types. also
known as the polymorphic lambda-calculus
or second-order lambda-calculus, it is an
extension of simply typed lambda-calculus.
It's as simple as a mocking bird... :)
Why do you care so much about simply-typed? If not as a foundation for
the theory of functional languages: yet xx is an object of interest in
its own right, simply beyond the simply-typed.
But in simple types itself, th self application
x x has no type. You can try yourself:
/* Typed Variable */
typeof(_:A, B) :-
unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
And then the query:
?- X=_:_, typeof((X*X), T).
false.
The query will though succeed if you remove
the occurs check.
Which is more interesting: what it is, not what it is not.
With plain unification (on SWI):
```
?- X=_:_, typeof((X*X), T).
X = _:_S1, % where
_S1 = (_S1->T).
```
That is also somewhat reminiscent of Coq's result, except that here the
type is a ground and cyclic term (a "cyclic type"?), as such not even polymorphic... Nor, OTOH, can I think of a way to construct a cyclic
term in Coq.
On 08/01/2025 19:21, Mild Shock wrote:
Julio wrote:
Why do you care so much about simply-typed?
What makes you think I care about simply-typed?
It was part of the MSE question you moron:
Can't you stay on topic?
Define topic.
-Julio
Why do you care so much about simply-typed?
I'm having trouble understanding the Wikipedia articlehttps://math.stackexchange.com/q/1927260/1482376
on Simply typed lambda calculus.
And also on the Curry-Howard Isomorphism. Is there a
nice way to put it in bird-forest form like To Mock
a Mocking Bird. This book made everything so simple
and intuitive for me.
On 08/01/2025 18:45, Julio Di Egidio wrote:
On 08/01/2025 10:31, Mild Shock wrote:
Julio Di Egidio schrieb:
On 08/01/2025 01:10, Mild Shock wrote:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
Define Smullyan.
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`. Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
F (T -> U) False (F T U).
```
Thats System F and not simple types. also
known as the polymorphic lambda-calculus
or second-order lambda-calculus, it is an
extension of simply typed lambda-calculus.
It's as simple as a mocking bird... :)
Why do you care so much about simply-typed? If not as a foundation
for the theory of functional languages: yet xx is an object of
interest in its own right, simply beyond the simply-typed.
But in simple types itself, th self application
x x has no type. You can try yourself:
/* Typed Variable */
typeof(_:A, B) :-
unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
And then the query:
?- X=_:_, typeof((X*X), T).
false.
The query will though succeed if you remove
the occurs check.
Which is more interesting: what it is, not what it is not.
With plain unification (on SWI):
```
?- X=_:_, typeof((X*X), T).
X = _:_S1, % where
_S1 = (_S1->T).
```
That is also somewhat reminiscent of Coq's result, except that here
the type is a ground and cyclic term (a "cyclic type"?), as such not
even polymorphic... Nor, OTOH, can I think of a way to construct a
cyclic term in Coq.
Correction: it's not really ground since T isn't...
-Julio
Hi,
You want definitions, here you got definitions.
In your case the Tool that makes you a Fool
is simply Coq. You don't know what you are doing!
Idiot = Julio the new Fool with Tool
Although I admit its interesting to see
that outside simply typed self application
exists. Even in System F.
But in System F it can make for example
∀F.F inhabitated. So it becomes logically
useless because anything can be proved.
Maybe you should use more your Brain and less Coq?
But I understand its your new medium. But please
do not forget that a simpler medium like
Prolog can also give you some insight.
Bye
Julio Di Egidio schrieb:
On 08/01/2025 19:21, Mild Shock wrote:
Julio wrote:
Why do you care so much about simply-typed?
What makes you think I care about simply-typed?
It was part of the MSE question you moron:
Can't you stay on topic?
Define topic.
-Julio
Julio wrote:
Why do you care so much about simply-typed?
What makes you think I care about simply-typed?
It was part of the MSE question you moron:
Can't you stay on topic?
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan https://www.youtube.com/watch?v=omz6SbUpFQ8
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Bye
You want definitions, here you got definitions.
In your case the Tool that makes you a Fool
is simply Coq. You don't know what you are doing!
Idiot = Julio the new Fool with Tool
Although I admit its interesting to see
that outside simply typed self application
exists. Even in System F.
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan https://www.youtube.com/watch?v=omz6SbUpFQ8
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Bye
On 08/01/2025 19:29, Mild Shock wrote:
You want definitions, here you got definitions.
In your case the Tool that makes you a Fool
is simply Coq. You don't know what you are doing!
Idiot = Julio the new Fool with Tool
Although I admit its interesting to see
that outside simply typed self application
exists. Even in System F.
That's actually where I don't really know what I am doing (system F is inconsistent?! do *you* know anything at all?): as for Coq, if one
doesn't know what one is doing in Coq, one doesn't know what formal
logic and/or plain programming is...
-Julio
Hi,
Although Simple Types can ban self application,
like making (x x) typeable is impossible. It cannot
completely ban the Curry Paradox,
since we can still derive:
?- between(1,16,N), search(typeof(X, [],
((a->(a->b))->(((a->b)->a)->b))), N, 0).
N = 15,
X = lam(lam(lam(0*(1*0))*lam(2*0*0))) .
This is a well known fact that in Minimal Logic
the Curry Paradox is still derivable. But what
about Affine Logic, can it ban the Curry Paradox?
I guess so, if Affine Logic ban contraction,
then Lambda Exprssions such as lam(0*(1*0)) and
lam(2*0*0) cannot be formed, since 0 apears twice.
But how rigorously show the conjecture that
Affine Logic bans the Curry Paradox?
Bye
Source code for the proof search with de Brujin
indexes, which requires a ternary typeof/3, since
we need also pass around a context L:
/* Implication Intro */
typeof(lam(Y), L, (A -> B)) :-
typeof(Y, [A|L], B).
/* Axiom */
typeof(K, L, B) :-
nth0(K, L, A),
unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), L, B) :-
typeof(S, L, (A -> B)),
typeof(T, L, A).
search(true, N, N).
search((A,B), N, M) :-
search(A, N, H),
search(B, H, M).
search(typeof(P, L, T), N, M) :- N>0, H is N-1,
clause(typeof(P, L, T), B),
search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
unify_with_occurs_check(A,B).
search(nth0(K, L, A), N, N) :-
nth0(K, L, A).
Mild Shock schrieb:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Bye
Hi,
More details on RAG, see here RETRO Project (*) at t=12:01:
What's wrong with LLMs and what we should be building instead
Tom Dietterich - 10.07.2023
https://youtu.be/cEyHsMzbZBs
So its not a very new technique now appearing in
generative AIs on the market as well. Some chat bots
are even now able to sometimes show more clearly the
used source documents in their answer. The MSE end
user can still edit a citation by hand to conform
more to the SEN format, if this would be the issue.
Also the MSE end user can explicitly now ask a chat
bot for sources, which he will get most of the time.
Or he can give a chat bot a source for review and
discussion. This works also. So there is not anymore
this "remoteness" of an LLM to the actual virtual
world of documents. Its more that they now inhabit the
actual virtual world and interact with it. Another issue
I see is that in certain countries and educational
institutions, it might the case that working with a
chat bot is something that the students learn,
yet they are not officially allowed to use it on
MSE, because MSE policies are based on outdated
views about generative AI.
See also:
(*) RETRO Project:
Improving language models by retrieving from trillions of tokens
Sebastian Borgeaud et al. - 7 Feb 2022
https://arxiv.org/abs/2112.04426
Bye
Mild Shock schrieb:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Bye
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 715 |
| Nodes: | 16 (0 / 16) |
| Uptime: | 170:11:58 |
| Calls: | 12,097 |
| Calls today: | 5 |
| Files: | 15,003 |
| Messages: | 6,517,850 |