🗊Презентация Fixed Points

Категория: Устройства и комплектующие
Нажмите для полного просмотра!
Fixed Points, слайд №1Fixed Points, слайд №2Fixed Points, слайд №3Fixed Points, слайд №4Fixed Points, слайд №5Fixed Points, слайд №6Fixed Points, слайд №7Fixed Points, слайд №8Fixed Points, слайд №9Fixed Points, слайд №10Fixed Points, слайд №11Fixed Points, слайд №12Fixed Points, слайд №13Fixed Points, слайд №14Fixed Points, слайд №15Fixed Points, слайд №16Fixed Points, слайд №17Fixed Points, слайд №18Fixed Points, слайд №19Fixed Points, слайд №20Fixed Points, слайд №21Fixed Points, слайд №22Fixed Points, слайд №23Fixed Points, слайд №24Fixed Points, слайд №25Fixed Points, слайд №26Fixed Points, слайд №27Fixed Points, слайд №28Fixed Points, слайд №29Fixed Points, слайд №30
Скачать
Вы можете ознакомиться и скачать презентацию на тему Fixed Points. Доклад-сообщение содержит 30 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1


7. Fixed Points
Описание слайда:
7. Fixed Points

Слайд 2


Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi
Описание слайда:
Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi

Слайд 3


References Paul Hudak, “Conception, Evolution, and Application of Functional Programming Languages,” ACM Computing Surveys 21/3, Sept. 1989, pp 359-411.
Описание слайда:
References Paul Hudak, “Conception, Evolution, and Application of Functional Programming Languages,” ACM Computing Surveys 21/3, Sept. 1989, pp 359-411.

Слайд 4


Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi
Описание слайда:
Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi

Слайд 5


Recall these encodings …
Описание слайда:
Recall these encodings …

Слайд 6


Representing Numbers There is a “standard encoding” of natural numbers into the lambda calculus:
Описание слайда:
Representing Numbers There is a “standard encoding” of natural numbers into the lambda calculus:

Слайд 7


Working with numbers What happens when we apply pred 0? What does this mean?
Описание слайда:
Working with numbers What happens when we apply pred 0? What does this mean?

Слайд 8


Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi
Описание слайда:
Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi

Слайд 9


Recursion Suppose we want to define arithmetic operations on our lambda-encoded numbers. In Haskell we can program: so we might try to “define”: plus   n m . iszero n m ( plus ( pred n ) ( succ m ) ) Unfortunately this is not a definition, since we are trying to use plus before it is defined. I.e, plus is free in the “definition”!
Описание слайда:
Recursion Suppose we want to define arithmetic operations on our lambda-encoded numbers. In Haskell we can program: so we might try to “define”: plus   n m . iszero n m ( plus ( pred n ) ( succ m ) ) Unfortunately this is not a definition, since we are trying to use plus before it is defined. I.e, plus is free in the “definition”!

Слайд 10


Recursive functions as fixed points We can obtain a closed expression by abstracting over plus: rplus   plus n m . iszero n m ( plus ( pred n ) ( succ m ) ) rplus takes as its argument the actual plus function to use and returns as its result a definition of that function in terms of itself. In other words, if fplus is the function we want, then: rplus fplus  fplus I.e., we are searching for a fixed point of rplus ...
Описание слайда:
Recursive functions as fixed points We can obtain a closed expression by abstracting over plus: rplus   plus n m . iszero n m ( plus ( pred n ) ( succ m ) ) rplus takes as its argument the actual plus function to use and returns as its result a definition of that function in terms of itself. In other words, if fplus is the function we want, then: rplus fplus  fplus I.e., we are searching for a fixed point of rplus ...

Слайд 11


Fixed Points A fixed point of a function f is a value p such that f p = p. Examples: fact 1 = 1 fact 2 = 2 fib 0 = 0 fib 1 = 1 Fixed points are not always “well-behaved”: succ n = n + 1 What is a fixed point of succ?
Описание слайда:
Fixed Points A fixed point of a function f is a value p such that f p = p. Examples: fact 1 = 1 fact 2 = 2 fib 0 = 0 fib 1 = 1 Fixed points are not always “well-behaved”: succ n = n + 1 What is a fixed point of succ?

Слайд 12


Fixed Point Theorem Theorem: Every lambda expression e has a fixed point p such that (e p)  p.
Описание слайда:
Fixed Point Theorem Theorem: Every lambda expression e has a fixed point p such that (e p)  p.

Слайд 13


How does Y work? Recall the non-terminating expression  = ( x . x x) ( x . x x)  loops endlessly without doing any productive work. Note that (x x) represents the body of the “loop”. We simply define Y to take an extra parameter f, and put it into the loop, passing it the body as an argument: Y   f . ( x . f (x x)) ( x . f (x x)) So Y just inserts some productive work into the body of 
Описание слайда:
How does Y work? Recall the non-terminating expression  = ( x . x x) ( x . x x)  loops endlessly without doing any productive work. Note that (x x) represents the body of the “loop”. We simply define Y to take an extra parameter f, and put it into the loop, passing it the body as an argument: Y   f . ( x . f (x x)) ( x . f (x x)) So Y just inserts some productive work into the body of 

Слайд 14


Using the Y Combinator What are succ and pred of (False, (Y succ))? What does this represent?
Описание слайда:
Using the Y Combinator What are succ and pred of (False, (Y succ))? What does this represent?

Слайд 15


Recursive Functions are Fixed Points We seek a fixed point of: rplus   plus n m . iszero n m ( plus ( pred n ) ( succ m ) ) By the Fixed Point Theorem, we simply take: plus  Y rplus Since this guarantees that: rplus plus  plus as desired!
Описание слайда:
Recursive Functions are Fixed Points We seek a fixed point of: rplus   plus n m . iszero n m ( plus ( pred n ) ( succ m ) ) By the Fixed Point Theorem, we simply take: plus  Y rplus Since this guarantees that: rplus plus  plus as desired!

Слайд 16


Unfolding Recursive Lambda Expressions
Описание слайда:
Unfolding Recursive Lambda Expressions

Слайд 17


Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi
Описание слайда:
Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi

Слайд 18


The Typed Lambda Calculus There are many variants of the lambda calculus. The typed lambda calculus just decorates terms with type annotations: Syntax: e ::= x | e12 1 e22 | ( x2.e1)2 1 Operational Semantics:
Описание слайда:
The Typed Lambda Calculus There are many variants of the lambda calculus. The typed lambda calculus just decorates terms with type annotations: Syntax: e ::= x | e12 1 e22 | ( x2.e1)2 1 Operational Semantics:

Слайд 19


Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi
Описание слайда:
Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi

Слайд 20


The Polymorphic Lambda Calculus Polymorphic functions like “map” cannot be typed in the typed lambda calculus! Need type variables to capture polymorphism:  reduction (ii): ( x . e11) e22  [2/] [e22/x] e11 Example:
Описание слайда:
The Polymorphic Lambda Calculus Polymorphic functions like “map” cannot be typed in the typed lambda calculus! Need type variables to capture polymorphism:  reduction (ii): ( x . e11) e22  [2/] [e22/x] e11 Example:

Слайд 21


Hindley-Milner Polymorphism Hindley-Milner polymorphism (i.e., that adopted by ML and Haskell) works by inferring the type annotations for a slightly restricted subcalculus: polymorphic functions. If: then is ok, but if then is a type error since the argument len cannot be assigned a unique type!
Описание слайда:
Hindley-Milner Polymorphism Hindley-Milner polymorphism (i.e., that adopted by ML and Haskell) works by inferring the type annotations for a slightly restricted subcalculus: polymorphic functions. If: then is ok, but if then is a type error since the argument len cannot be assigned a unique type!

Слайд 22


Polymorphism and self application Even the polymorphic lambda calculus is not powerful enough to express certain lambda terms. Recall that both  and the Y combinator make use of “self application”:  = ( x . x x ) ( x . x x ) What type annotation would you assign to ( x . x x)?
Описание слайда:
Polymorphism and self application Even the polymorphic lambda calculus is not powerful enough to express certain lambda terms. Recall that both  and the Y combinator make use of “self application”:  = ( x . x x ) ( x . x x ) What type annotation would you assign to ( x . x x)?

Слайд 23


Built-in recursion with letrec AKA def AKA µ Most programming languages provide direct support for recursively-defined functions (avoiding the need for Y)
Описание слайда:
Built-in recursion with letrec AKA def AKA µ Most programming languages provide direct support for recursively-defined functions (avoiding the need for Y)

Слайд 24


Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi
Описание слайда:
Roadmap Representing Numbers Recursion and the Fixed-Point Combinator The typed lambda calculus The polymorphic lambda calculus Other calculi

Слайд 25


Featherweight Java
Описание слайда:
Featherweight Java

Слайд 26


Other Calculi Many calculi have been developed to study the semantics of programming languages. Object calculi: model inheritance and subtyping .. lambda calculi with records Process calculi: model concurrency and communication CSP, CCS, pi calculus, CHAM, blue calculus Distributed calculi: model location and failure ambients, join calculus
Описание слайда:
Other Calculi Many calculi have been developed to study the semantics of programming languages. Object calculi: model inheritance and subtyping .. lambda calculi with records Process calculi: model concurrency and communication CSP, CCS, pi calculus, CHAM, blue calculus Distributed calculi: model location and failure ambients, join calculus

Слайд 27


A quick look at the π calculus
Описание слайда:
A quick look at the π calculus

Слайд 28


What you should know! Why isn’t it possible to express recursion directly in the lambda calculus? What is a fixed point? Why is it important? How does the typed lambda calculus keep track of the types of terms? How does a polymorphic function differ from an ordinary one?
Описание слайда:
What you should know! Why isn’t it possible to express recursion directly in the lambda calculus? What is a fixed point? Why is it important? How does the typed lambda calculus keep track of the types of terms? How does a polymorphic function differ from an ordinary one?

Слайд 29


Can you answer these questions? How would you model negative integers in the lambda calculus? Fractions? Is it possible to model real numbers? Why, or why not? Are there more fixed-point operators other than Y? How can you be sure that unfolding a recursive expression will terminate? Would a process calculus be Church-Rosser?
Описание слайда:
Can you answer these questions? How would you model negative integers in the lambda calculus? Fractions? Is it possible to model real numbers? Why, or why not? Are there more fixed-point operators other than Y? How can you be sure that unfolding a recursive expression will terminate? Would a process calculus be Church-Rosser?

Слайд 30


License http://creativecommons.org/licenses/by-sa/3.0/
Описание слайда:
License http://creativecommons.org/licenses/by-sa/3.0/

Скачать

Теги Fixed Points
Похожие презентации
Mypresentation.ru
Загрузить презентацию