Difference between revisions of "Dana Scott on Lambda Calculus"

From PKC
Jump to navigation Jump to search
m (Text replacement - "{{#ev:youtube |" to "{{#widget:YouTube |id=")
 
(34 intermediate revisions by the same user not shown)
Line 1: Line 1:
Prof. Dana Scott gave a few talks on Lambda Calculus, and some of them are available on Youtube.
Prof. Dana Scott gave a few talks on [[Lambda Calculus]], and some of them are available on Youtube.


A list of them can be found here:
A list of them can be found here:
Line 37: Line 37:


=Lecture 3=
=Lecture 3=
This lecture<ref name="Scott Part 3">{{:Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5 - λC 2017}}</ref> starts to mention the notion of [[algebraic closure]] and [[fixed point]]s.
This lecture<ref name="Scott Part 3">{{:Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5 - λC 2017}}</ref> starts to mention the notion of [[algebraic closure]] and [[fixed point]]s.


=Lecture 4=
==Drawing of Lattice==
This lecture<ref name="Scott Part 4">{{:Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5 - λC 2017}}</ref><ref extends="Scott Part 4">[https://youtu.be/8zk0yS8Jp5w?t=1200 On Recursive Enumeration]</ref> mentioned three important persons in logic.  
He mentioned<ref>[https://youtu.be/8zk0yS8Jp5w?t=236 Every undergraduate should do exercises in proving continuous functions]</ref> that every undergraduate should learn to prove continuity in functions as an exercise.
 
This lecture<ref extends="Scott Part 3">[https://youtu.be/8zk0yS8Jp5w?t=1200 On Recursive Enumeration]</ref> mentioned three important persons in logic.  
#John Myhill
#John Myhill
#John Sheperdson
#John Sheperdson
Line 49: Line 52:
# [https://youtu.be/8zk0yS8Jp5w?t=1300 Here is where he wants to kick himself at the night]
# [https://youtu.be/8zk0yS8Jp5w?t=1300 Here is where he wants to kick himself at the night]
# [https://youtu.be/8zk0yS8Jp5w?t=1330 No body said: "do this operators have any algebra to them...", if only, if only ...]
# [https://youtu.be/8zk0yS8Jp5w?t=1330 No body said: "do this operators have any algebra to them...", if only, if only ...]
This statement relates to the paper<ref>{{:Paper/Algebra of Systems}}</ref> on [[Algebra of Systems]] and this statement in particulary<ref>[[Algebra of Systems|A small algebra is feasible ...]]</ref>.
This statement relates to the paper<ref name="AoS">{{:Paper/Algebra of Systems}}</ref> on [[Algebra of Systems]] and this statement in particular.<ref>[[Algebra of Systems#A Concise Algebra for automating engineering tasks|A Concise Algebra for automating engineering tasks]]</ref>.
 
==A Concise Algebra for automating engineering tasks==
This year 2009 paper<ref name="AoS"/> summarized the following statement in the conclusion:
In [[Laws of programming]]<ref>{{:Paper/Laws of programming}}</ref>, Hoare et al. questioned whether a small set of algebraic laws can be directly useful in a practical engineering design problem. The absence of a tool that can bridge the cognitive gap between mathematical abstractions and engineering problems may have been the main reason for their conservative attitude.
The above statement echos who [[Dana Scott]]<ref>[https://youtu.be/8zk0yS8Jp5w?t=1300 Scott Commenting on a small algebra for combinators]</ref> was saying in the 2018 Lambda Conference.
 
==A lookup table as a enumerable function==
He said in this lecture<ref>[https://youtu.be/8zk0yS8Jp5w?t=1468 If the giant lookup table is enumerable ...]</ref>:
If that lookup table is enumerable, that is a good definition of say that the enumeration operation is computable. ... So that computability here is on the same plane with enumerability.
<noinclude>
 
==Always think positively==
He said the following<ref>[https://youtu.be/8zk0yS8Jp5w?t=1860 Always think positively]</ref>:
Don't think of divergence and all of that. ... You can only achieve what can possibly achieve. Don't think of things that cannot be done. This is the way how enumeration works. Working with the positives. Of course, you can think of complementary sets.
This is also where one can starting relating to the laws of [[composition]].
 
==Lambda Calculus allows you to notate Least Fixed Points==
There is a '''well-foundedness''' as he mentioned at about [https://youtu.be/8zk0yS8Jp5w?t=2340 39 minutes] into this video. He started talking about <ref>[https://youtu.be/8zk0yS8Jp5w?t=2380 Least Fixed Point and Lambda Calculus]</ref>. There is a connection between <math>lfp(x)</math> or Least Fixed Point of <math>x</math>, and lambda calculus.
 
==All Computable/Continuous Functions can be composed using Lambda Calculus==
This where things get related to [[composition]]<ref>[https://youtu.be/8zk0yS8Jp5w?t=2485 All continuous functions can be composed of Lambda Calculus]</ref>.
All Computable/Continuous Functions can be composed using Lambda Calculus and arithmetics. Arithmetics gives you the power of analyzing Gödel numbers and other kinds of structures.
 
==Number 0,1 is related to K and S respectively==
The arithmetic mechanism can be represented using [[SK Combinators]], therefore, each can be related to a specific kind of number<ref>[https://youtu.be/8zk0yS8Jp5w?t=2555 S and K as numbers 1 and 0 respectively]</ref>. The smaller numbers<code>2, 3, 4</code> are assigned to do arithmetics.


==Sub models with Closure Conditions within Computable Recursive Operators==
There are ways to take closures in sub [https://youtu.be/8zk0yS8Jp5w?t=2978 Lambad Calculus and iteration gives you recursive theory]. It also allows one to filter out certain elements.
Closure is something can be expressed in Lambda Calculus<ref>[https://youtu.be/8zk0yS8Jp5w?t=2973 Closure expressed in Lambda Calculus]</ref>.


==Closed elements in the closed ... forms an algebra==
[https://youtu.be/8zk0yS8Jp5w?t=3310 Closed elements forms ...]
The last few minutes of lecture 3, Scott showed that there is a strong connection between algebra, complete [[lattice]], upper/lower bounds as [[closure]], and finally, [[fixed point]].


=Lecture 4=
There are two uses of Close here<ref>[https://youtu.be/3ejEdS_iQDk?t=186 There are two uses of Close Here]</ref>.
# Fixed Point Operator: Fixed Point of Something that cannot be fixed up anymore by C that is already fixed.
# The Totality of Fixed Point of C form a Topological Space. In fact, it is the subspace of Power Set of <math>n</math> with a power set of '''[[anthropology]]'''? In other words, it's a restriction on the topology of the power set of n- a topology on a sub lattice. And those topological spaces can be put together in at the category different closure operators give you different subspaces and continuous mapping between the subspaces that can be explained entirely in our lambda calculus.
# Now the key thing her is: '''All''' computable continuous functions can be composed by using Lambda Calculus and arithmetic. Arithmetic gives you the possibility of analyzing Godel numbers as other kinds of structures. Lambda calculus only uses a fraction of the power of Godel numbering.<ref>[https://youtu.be/8zk0yS8Jp5w?t=2485 All computable functions can be represented in Lambda Calculus]</ref>
# The basic operations of Lambda Calculus and arithmetic, when done over and over again, give you all [[recursively enumerable set]]s.<ref>[https://youtu.be/8zk0yS8Jp5w?t=2633 Lambda Calculus and arithmetic Lambda Calculus and arithmetic ... give you all recursively enumerable sets.]</ref>
# We can also think of doing these computations with resource limited means. Suppose you choose only Godel numbers that can fit into the state of Colorado, so you will only get a finite approximation to what you can do if you limit your Godel numbers. <ref>[https://youtu.be/8zk0yS8Jp5w?t=2736 Finite approximation to what you can do if you limit your Godel numbers.] </ref>
# I hate programming Turing machines, even Turing himself made a number of mistakes in his original paper that had to be corrected later. The programs are hard to write because of the very limited means of running back and forth on the tape to do Turing machines. But this is much less to write down.<ref>[https://youtu.be/8zk0yS8Jp5w?t=2840 I hate programming Turing machines, even Turing himself made a number of mistakes in his original paper.]</ref>.
<noinclude>
<noinclude>
# Ross's found an improvement to Godel's incompleteness theorem. [https://youtu.be/8zk0yS8Jp5w?t=2925 Barkley Rosser found an improvement to Godel's incompleteness theorem.]
# [https://youtu.be/8zk0yS8Jp5w?t=3105 In an abstract way, closure is something you can express it nicely in Lambda Calculus]. A closure operator is an operator such that from the generator <math>X</math> you expand from the closure of  <math>X</math>.
# [https://youtu.be/8zk0yS8Jp5w?t=3500 On these lattices, you can take the analogy of the Power set and make the fixed point of C a topological space and the Lambda Calculus gives you a notation for all the continuous functions between those lattices.]
# So you see: [https://youtu.be/8zk0yS8Jp5w?t=3526 The Godel numbers give you the possibility of thinking of any kind of finite structure. But you can now look down at specialized structure, and special ways. And so these closure operators give you a way of doing a lot of that.]
=Lecture 5=
# But here is the crazy thing that Rosser discovered here: [https://youtu.be/llWiPFx893k?t=782 If you iterate iterating, what do you get?] Exponential<ref>{{:Video/Category Theory for the Working Hacker by Philip Wadler}}</ref>?
{{#widget:YouTube
|id=V10hzjgoklA|||||start=2317
}}


=References=
=References=
Line 61: Line 114:
[[Category:Logic]]
[[Category:Logic]]
[[Category:Lambda Calculus]]
[[Category:Lambda Calculus]]
[[Category:Meta Programming]]
[[Category:Gödel Number]]
[[Category:Gasing Method]]
</noinclude>
</noinclude>

Latest revision as of 10:50, 26 August 2022

Prof. Dana Scott gave a few talks on Lambda Calculus, and some of them are available on Youtube.

A list of them can be found here:

Local Links
Video/Dana S. Scott Lambda Calculus, Then and Now
Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 1) - λC 2018
Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 2) - λC 2018
Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 3) - λC 2018
Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 4) - λC 2018
Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 5) - λC 2018
Video/Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 6) - λC 2018
Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 1 of 5 - λC 2017
Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 2 of 5 - λC 2017
Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5 - λC 2017
Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5 - λC 2017
Video/Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5 - λC 2017
Video/Stochastic Lambda-Calculus

This video series seems to be taken in the same day, a total of 5 hours. Prof. Scott offered many anecdotal insights on how calculus was invented and formed. It directly relates to the notion of function and combinators. Particularly, the SK Combinators.

Lecture 1

This starting lecture talks about the name of Lambda came from[1].

Lecture 2

Godel Numbering

Think about variables in terms of special numbers. This is an insight from Godel[2]Cite error: Invalid <ref> tag; invalid names, e.g. too many, and later utilized to created Universal computation.

We don't need Turing Machine

In this lectureCite error: Invalid <ref> tag; invalid names, e.g. too many, Scott explicitly stated that: 

"You don't need Turing Machine to understand it, I hope I can convince you of that."

Scott's Universe is the Powerset of Integers

In this lectureCite error: Invalid <ref> tag; invalid names, e.g. too many, Scott explicitly stated that: 

"The Universe if the Powerset of Integers."

Sophomores or Juniors should learn some Topology

Sophomores or juniors should have some topology from calculus...

A neighborhood of a possibly infinite set...

Once you define Topology, you may define continuous functions

Lecture 3

This lecture[3] starts to mention the notion of algebraic closure and fixed points.

Drawing of Lattice

He mentioned[4] that every undergraduate should learn to prove continuity in functions as an exercise.

This lectureCite error: Invalid <ref> tag; invalid names, e.g. too many mentioned three important persons in logic.

  1. John Myhill
  2. John Sheperdson
  3. Hartley Rogers Jr.

Why he kicks himself in the middle of the night

This is also the place where he starts talking about the recursive combinators, and how this enumerative device can be used to make one rich and famous.

  1. Here is where he wants to kick himself at the night
  2. No body said: "do this operators have any algebra to them...", if only, if only ...

This statement relates to the paper[5] on Algebra of Systems and this statement in particular.[6].

A Concise Algebra for automating engineering tasks

This year 2009 paper[5] summarized the following statement in the conclusion: 

In Laws of programming[7], Hoare et al. questioned whether a small set of algebraic laws can be directly useful in a practical engineering design problem. The absence of a tool that can bridge the cognitive gap between mathematical abstractions and engineering problems may have been the main reason for their conservative attitude.

The above statement echos who Dana Scott[8] was saying in the 2018 Lambda Conference.

A lookup table as a enumerable function

He said in this lecture[9]: 

If that lookup table is enumerable, that is a good definition of say that the enumeration operation is computable. ... So that computability here is on the same plane with enumerability.


Always think positively

He said the following[10]: 

Don't think of divergence and all of that. ... You can only achieve what can possibly achieve. Don't think of things that cannot be done. This is the way how enumeration works. Working with the positives. Of course, you can think of complementary sets.

This is also where one can starting relating to the laws of composition.

Lambda Calculus allows you to notate Least Fixed Points

There is a well-foundedness as he mentioned at about 39 minutes into this video. He started talking about [11]. There is a connection between or Least Fixed Point of , and lambda calculus.

All Computable/Continuous Functions can be composed using Lambda Calculus

This where things get related to composition[12]. 

All Computable/Continuous Functions can be composed using Lambda Calculus and arithmetics. Arithmetics gives you the power of analyzing Gödel numbers and other kinds of structures.

Number 0,1 is related to K and S respectively

The arithmetic mechanism can be represented using SK Combinators, therefore, each can be related to a specific kind of number[13]. The smaller numbers2, 3, 4 are assigned to do arithmetics.

Sub models with Closure Conditions within Computable Recursive Operators

There are ways to take closures in sub Lambad Calculus and iteration gives you recursive theory. It also allows one to filter out certain elements. 

Closure is something can be expressed in Lambda Calculus[14].

Closed elements in the closed ... forms an algebra

Closed elements forms ... The last few minutes of lecture 3, Scott showed that there is a strong connection between algebra, complete lattice, upper/lower bounds as closure, and finally, fixed point.


Lecture 4

There are two uses of Close here[15].

  1. Fixed Point Operator: Fixed Point of Something that cannot be fixed up anymore by C that is already fixed.
  2. The Totality of Fixed Point of C form a Topological Space. In fact, it is the subspace of Power Set of with a power set of anthropology? In other words, it's a restriction on the topology of the power set of n- a topology on a sub lattice. And those topological spaces can be put together in at the category different closure operators give you different subspaces and continuous mapping between the subspaces that can be explained entirely in our lambda calculus.
  3. Now the key thing her is: All computable continuous functions can be composed by using Lambda Calculus and arithmetic. Arithmetic gives you the possibility of analyzing Godel numbers as other kinds of structures. Lambda calculus only uses a fraction of the power of Godel numbering.[16]
  4. The basic operations of Lambda Calculus and arithmetic, when done over and over again, give you all recursively enumerable sets.[17]
  5. We can also think of doing these computations with resource limited means. Suppose you choose only Godel numbers that can fit into the state of Colorado, so you will only get a finite approximation to what you can do if you limit your Godel numbers. [18]
  6. I hate programming Turing machines, even Turing himself made a number of mistakes in his original paper that had to be corrected later. The programs are hard to write because of the very limited means of running back and forth on the tape to do Turing machines. But this is much less to write down.[19].
  1. Ross's found an improvement to Godel's incompleteness theorem. Barkley Rosser found an improvement to Godel's incompleteness theorem.
  2. In an abstract way, closure is something you can express it nicely in Lambda Calculus. A closure operator is an operator such that from the generator you expand from the closure of .
  3. On these lattices, you can take the analogy of the Power set and make the fixed point of C a topological space and the Lambda Calculus gives you a notation for all the continuous functions between those lattices.
  4. So you see: The Godel numbers give you the possibility of thinking of any kind of finite structure. But you can now look down at specialized structure, and special ways. And so these closure operators give you a way of doing a lot of that.

Lecture 5

  1. But here is the crazy thing that Rosser discovered here: If you iterate iterating, what do you get? Exponential[20]?

References

  1. ↑ Scott, Dana (Oct 12, 2017). Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 1 of 5 - λC 2017. local page: LambdaConf. 
  2. ↑ Scott, Dana (Oct 12, 2017). Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 2 of 5 - λC 2017. local page: LambdaConf. 
  3. ↑ Scott, Dana (Oct 12, 2017). Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5 - λC 2017. local page: LambdaConf. 
  4. ↑ Every undergraduate should do exercises in proving continuous functions
  5. ↑ 5.0 5.1 Koo, Hsueh-Yung Benjamin; Simmons, Willard; Crawley, Edward (Nov 16, 2021). "Algebra of Systems as a Meta Language for Model Synthesis and Analysis" (PDF). local page: IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS. 
  6. ↑ A Concise Algebra for automating engineering tasks
  7. ↑ Hoare, C. A. R.; Hayes, I. J.; He, Jifeng; Morgan, C. C.; Roscoe, A. W.; Sanders, J. W.; Sorensen, I. H.; Spivey, J. M.; Sufrin, B. A. (Aug 1987). "Laws of Programming" (PDF). 30 (8). local page: ACM. 
  8. ↑ Scott Commenting on a small algebra for combinators
  9. ↑ If the giant lookup table is enumerable ...
  10. ↑ Always think positively
  11. ↑ Least Fixed Point and Lambda Calculus
  12. ↑ All continuous functions can be composed of Lambda Calculus
  13. ↑ S and K as numbers 1 and 0 respectively
  14. ↑ Closure expressed in Lambda Calculus
  15. ↑ There are two uses of Close Here
  16. ↑ All computable functions can be represented in Lambda Calculus
  17. ↑ Lambda Calculus and arithmetic Lambda Calculus and arithmetic ... give you all recursively enumerable sets.
  18. ↑ Finite approximation to what you can do if you limit your Godel numbers.
  19. ↑ I hate programming Turing machines, even Turing himself made a number of mistakes in his original paper.
  20. ↑ Wadler, Philip (Nov 11, 2016). Category Theory for the Working Hacker by Philip Wadler. local page: Lambda World. 

Related Pages

Retrieved from "https://pkc.pub/index.php?title=Dana_Scott_on_Lambda_Calculus&oldid=34737"