[go: up one dir, main page]
Scribd
Upload
15 views56 pages

Lecture01 DK

Key Concepts Computation is Functional Programming as an Explanatory Process Types, Values, and Expressions Typing and Evaluation rules Integers, Reals, Booleans, Products Parallelism, Work, and Span Referential Transparency and Extensional Equivalence Declaration Binding Scope (by the scope of a binding we mean the part of the code where that binding is visible/accessible) Environment Definition of a total function

Uploaded by

Zone
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
15 views56 pages

Lecture01 DK

Key Concepts Computation is Functional Programming as an Explanatory Process Types, Values, and Expressions Typing and Evaluation rules Integers, Reals, Booleans, Products Parallelism, Work, and Span Referential Transparency and Extensional Equivalence Declaration Binding Scope (by the scope of a binding we mean the part of the code where that binding is visible/accessible) Environment Definition of a total function

Uploaded by

Zone
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 56

15-150

Fall 2024
Dilsun Kaynar

LECTURE 1

Introduction,Philosophy, Some Basics


About 15-150
Instructors: Stephanie Balzer, Dilsun Kaynar
19 TAs

http://www.cs.cmu.edu/~15150/

We are on Canvas!
Today

• Organization of the course


• Philosophy of the course
• Basics of types, values, expressions in
SML
Course tasks
• Assignments 40%
• Labs 10%
• Midterm 1 15% (Sep 26)
• Midterm 2 15% (Nov 7)
• Final 20%
Collaboration policy

• Make sure to read and understand the


policy for this semester
Extra help
• Of ce Hours by TAs
• Instructors available by appointment
• Student Academic Success Center
• Drop-in Tutoring
• Wednesdays POS 280
• 1-on-1 tutoring by appointment
fi
Course philosophy

• Computation is functional.
• Programming is an explanatory
linguistic process.
Functional
programming

SML
Computation is
functional
• values classi ed with respect to types
• expressions
• functions map values to values
fi
Imperative vs. Functional
command expression

executed evaluated

has an effect no effect

x := 5 3 + 5

(new state) (new value)


Programming as
explanation
• Problem statement

}
• Invariants
High expectation to explain
• Speci cations precisely and concisely

• Proofs of correctness
• Analyze, decompose and t, prove
fi
fi
Parallelism

How many people have taken 15-122?

Let’s count it using parallelism.


Parallelism
/\
< 1, 0, 0, 1, 1 > 3
< 1, 0, 1, 0, 1 > 3
< 1, 1, 0, 1, 1 > 4

< 0, 0, 0, 1, 1 > 2
\/

12
sum: int sequence → int

type row = int sequence

type room = row sequence

fun count (class: room): int = sum (map sum class)


Analysis
• How could you improve the running time of
count?

Divide and conquer


Parallelism
• Expression evaluation has no side-e ects
• can evaluate independent code in parallel
• evaluation order has no effect on value

• Parallel evaluation may be faster than sequential

Learn to exploit parallelism!


ff
Cost Analysis
Work
• Sequential computation
• Total sequential time; number of operations

Span
• Parallel computation
• How long would it take if one could have as many
processors as one wants; length of longest critical
path
Introducing ML

• Types t
• Expressions e
• Values v (subset of expressions)
Examples
(3 + 4) * 2
1
==> 7 * 2
1
==> 14

(3 + 4) * (2 + 1)
3
==> 21

How many steps would the second take if we used parallelism?


"the " + "walrus"
==> "the walrus"

"the walrus" + 1 ill-typed

SML never evaluates an ill-typed expression!


Types, Expressions,
Values
• A type is a “prediction” about the kind of value
that an expression will have if it winds up having
a value
• An expression is well-typed if it has at least
one type, and ill-typed otherwise.
• A well-typed expression has a type, may have a
value, and may have an effect (not for our
effect-free fragment)
Every well-formed ML expression e

• has type t, written as e : t


• may have a value, written as e ↪ v
(or e ==> v)
• may have an effect (not our effect-free
fragment)
Example:

(3 + 4) * 2 : int
(3 + 4) * 2 ↪ 14
Types in ML
• Basic types
• int, real, bool, char, string
• Constructed types
• Product types
• Function types
• User-de ned types
fi
Integers, Expressions
• Type int
• Values …, ~1, 0, 1, …,
• Expressions e1 + e2, e1 - e2, e1 * e2,
e1 div e2, e1 mod e2, …
• Example ~4 * 3
Integers, Typing
• Typing rules
• n : int
• e1 + e2 : int if e1 : int and e2 : int
• similar for other operations

(3 + 4) * 2 : int because
(3 + 4): int 2: int
(3 + 4): int because 3: int and 4: int
Integers, Evaluation
1 1

• e1 + e2 ==> e1' + e2 if e1 ==> e1’


1 1
• n1 + e2 ==> n1 + e2’ if e2 ==> e2’
1
• n1 + n2 ==> n
where n is the sum of n1 and n2
Example
Well-typed expression with no value

5 div 0 : int
Notation Recap
e: t e has type t

e ==> e’ e reduces to e’

e↪ v e evaluates to v
Extensional
equivalence
≅
An equivalence relation on expressions of the same type
Extensional Equivalence

• Expressions of type int are extensionally


equivalent whenever one of the following is true
• if they evaluate to the same integer
• if they both loop forever
• if they both raise the same exception

Equivalence is a form of semantic equality


Equivalence

• Functions of type int -> int are extensionally


equivalent if they map extensionally equivalent
arguments to extensionally equivalent results
Referential
transparency
for types and values

• The type of an expression depends only


on the types of its sub-expressions
• The value of an expression depends only
on the values of its sub-expressions

safe substitution,
compositional reasoning
Extensional Equivalence

• Expressions of type int are extensionally


equivalent whenever one of the following is true
• if they evaluate to the same integer
• if they both loop forever
• if they both raise the same exception

For now, we will mostly focus on the rst


condition by making appropriate assumptions.
fi
Equivalence
21 + 21 ≅ 42 ≅ 7 * 6

[2,4,6] ≅ [1+1, 2+2, 3+3]

(fn x => x + x) ≅ (fn x => 2 * x)


Types in ML
• Basic types
• int, real, bool, char, string
• Constructed types
• Product types
• Function types
• User-de ned types
fi
Products, Expressions

• Types t1 * t2 for any type t1 and t2


• Values (v1, v2) for values v1 and v2
• Expressions (e1, e2), # e1, # e2 usually bad
style
• Example (~4 * 3, true)
(3,5,"another example")
Products, Typing

• (e1, e2) : t1 * t2 if e1 : t1 and e2 : t2


• Example
(~4 * 3, true): int * bool
(3,5,"another example"):
int * int * string
Products, Evaluation
1 1
• (e1 , e2) ==> (e1’ , e2) if e1 ==> e1’
1 1
• (v1 , e2) ==> (v1 , e2’) if e2 ==> e2’
1

• (v1 , v2) ==> (v1 , v2)


Evaluation:
(3*4, 1.1+7.2, true)
==> (12, 1.1+7.2, true)
==> (12, 8.3, true)

We could also write:

(3*4, 1.1+7.2,true) ↪ (12, 8.3,true)


Exercises
What are the type and values of the following expressions?
Type Value

(3*4, 1.1+7.2,true) int * real * bool (12,8.3,true)

int * int No value


(5 div 0, 2+1)

(5 + "8 miles", false) ill-typed No value

(2, (true,"a"), 3.1) int * (bool * string) * real (2, (true,"a"), 3.1)
Functions
In math, one talks about a function f being a mapping
between spaces X and Y.

In SML, we do the same with X and Y being types.


Declarations,
Environments, Scope
Declaration
val pi : real = 3.14

keyword identi er type value

Introduces binding of 3.14 to pi, sometimes written as [3.14/x]

Lexically statically scoped


fi
Environment
val x : int = 8 - 5 [3/x]
val y : int = x + 1 [4/y]
Environment
val x : int = 8 - 5 [3/x]
val y : int = x + 1 [4/y]
val x : int = 10 [10/x]
val z : int = x + 1 [11/z]

Second binding of x shadows rst binding. First binding has been shadowed.
fi
Local declarations
let
val m : int = 3
val n : int = m * m
in
m + n
end

This is an expression with type int and value 12.


Local declarations
val k : int = 4

}
let
val k : real = 3.0
in Type?
k * k Value?
end
Local declarations
val k : int = 4

}
let
val k : real = 3.0
in Type?
k * k Value?
end
9.0 : real
k
} Type?
Value?
4 : int
Concrete Type
De nitions
type float = real
type point = float * float
val p : point = (1.0, 2.6)
fi
Functions
Function declaration
(* square : int -> int
REQUIRES: true
ENSURES: square(x) evaluates to x * x
*)

fun square (x : int) : int = x * x

function name function body


Closures
Function declarations also create bindings:

fun square (x : int) : int = x * x

binds the identi er square to a closure:

[ /square]

Lambda expression fn x:int => x * x


Environment (all prior bindings when square was declared)
fi
5-step methodology
• Function name and type
• REQUIRES,
• ENSURES
• Function body
• Tests Step 6: Proof
How does ML evaluate
a function application e2
• Evaluate e to a function value f
2

• Reduce e to a value v
1

• Locally extend the environment that existed


at the time of the de nition of f with a
binding of value v to the variable x

• Evaluate the body in the resulting


environment
fi
To Do Tonight
• Canvas
• Assignments
• Set up lab

You might also like