Difference between revisions of "Dana Scott on Lambda Calculus"
| Line 50: | Line 50: | ||
This statement relates to the paper<ref>{{: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>. | This statement relates to the paper<ref>{{: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>. | ||
{{:Algebra of Systems#A Concise Algebra for automating engineering tasks}} | {{:Algebra of Systems#A Concise Algebra for automating engineering tasks}} | ||
==A Concise Algebra for automating engineering tasks== | |||
This year 2009 paper 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]]. | |||
Revision as of 06:16, 20 January 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:
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...
- The neighborhood of a possibly infinite set is just determined by a finite subset... and its complement
- A stronger topology, called product topology, where its complement can also be expressed with finite information... Hausdorf set taking half the topology
Once you define Topology, you may define continuous functions
- Define Continuous Functions
- The main difficulty is that there are two quantifiers, forming a rational number
- Finite amount of information can only be represented by a finite amount of rational numbers
Lecture 3
This lecture[3] starts to mention the notion of algebraic closure and fixed points.
This lectureCite error: Invalid <ref> tag; invalid names, e.g. too many mentioned three important persons in logic.
- John Myhill
- John Sheperdson
- 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.
- Here is where he wants to kick himself at the night
- No body said: "do this operators have any algebra to them...", if only, if only ...
This statement relates to the paper[4] on Algebra of Systems and this statement in particular.[5]. Algebra of Systems[6] is a many-sorted algebra, a computable data format that is summarized in a 2009 paper based on Koo's 2005 doctoral thesis[7].
A Concise Algebra for automating engineering tasks
This year 2009 paper summarized the following statement in the conclusion:
In Laws of programming[8], 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[9] was saying in the 2018 Lambda Conference.
Brendan Fong's doctorial thesis[10] on The Algebra of Open and Interconnected Systems is a rigorous treatment to the subject matter on AoS.
A lookup table as a enumerable function
He said in this lecture[11]:
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.
A Concise Algebra for automating engineering tasks
This year 2009 paper summarized the following statement in the conclusion:
In Laws of programming[12], 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[13] was saying in the 2018 Lambda Conference.
A lookup table as a enumerable function
He said in this lecture[14]:
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[15]:
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 [16]. 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[17].
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.
The arithmetic mechanism can be represented using SK Combinators, therefore, each can be related to a specific kind of number[18]. 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[19].
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.
References
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ A Concise Algebra for automating engineering tasks
- ↑ 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.
- ↑ Koo, Hsueh-Yung Benjamin (31 Jan 2005). A Meta-language for Systems Architecting (PDF) (Ph.D.). local page: MIT. Retrieved July 18, 2021.
- ↑ 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.
- ↑ Scott Commenting on a small algebra for combinators
- ↑ Fong, Brendan (2016). The Algebra of Open and Interconnected Systems (PDF) (Ph.D.). local page: University of Oxford. Retrieved October 15, 2021.
- ↑ If the giant lookup table is enumerable ...
- ↑ 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.
- ↑ Scott Commenting on a small algebra for combinators
- ↑ If the giant lookup table is enumerable ...
- ↑ Always think positively
- ↑ Least Fixed Point and Lambda Calculus
- ↑ All continuous functions can be composed of Lambda Calculus
- ↑ S and K as numbers 1 and 0 respectively
- ↑ Closure expressed in Lambda Calculus