about the last lecture that was this rules for for the lambda terms

so there was the introduction and elimination as I said so we had something like p and x

no sorry the introduction for lambda just has had one premise

and then we could derive I don't remember I probably call it at lambda intro a to b so this

intuition about introduction elimination it refers to types and not to terms so we have

product introduction because we have products and here we have lambda introduction because we have

an error in a type so if we change the type then accordingly you we have the corresponding rules

for introduction elimination of terms so that could be called lambda introduction and this p

say f from a to b so this produces f of p of type B this can be called lambda elimination or error

elimination so in in the glowing course we had this elimination introduction rules referring to

the connectivities and the connectivities are here on the level of type so we have this this

arrow we could just have this arrow elimination rule or arrow introduction rule okay and we are

introduced terms and context and so this context is a technical tool which is going to use but we

don't need it all the time so we can talk about terms and we say

that we also use them freely if we just don't need the context and then we can use the term

and just using this means that the construction t in this in some context is derivalable for some

gamma and for some return type so after all this preliminary is about operational semantics I

guess it's not difficult for you would be to give an operational semantics for this calculus for

this PCF language which introduced last but there are a couple of subtleties so perhaps I give some

rules and not all and first I consider as called by name operational semantics so for example

for example if I want to tell what the semantics of a pair is what I do I evaluate p say to c1

and evaluate q say to c2 and then p the pair p and q overlays to c1 and c2 and this is a case

where laziness doesn't help me because if I need to know what the result of a pair is I need to

evaluate both components of the pair and this contrast the case was the projection so if I

want to calculate pr1 of PC well actually in this case it doesn't help too so I evaluate p2 to a

pair c and d and then the projection of relates to c so I must have specified these things of

course on the right hand side hand side a value as a buddhan or a natural or

just this unit element or a pair of or a pair of values so this is the definition of the things

I evaluate to so I need to make sure that all the rules that I'm giving they are producing values

so this is the in the actual definition of course because a pair of values refers to values so I can

form tuples and do this inductively and this is important here for example and where laziness

helped me helps me actually as this rule if if I consider this construction if be than p else q

and I know that be able it's a true and p ever leads to see then the whole thing ever leads to see

this is lazy because I don't evaluate q if if I'm if I related the condition and it's true then

I immediately proceed to this branch and check it and I don't care about this branch it may

diverge but I will not notice it because I don't relate it then there is a rule for for the case

if B is false then I only check q and this is non symmetric

so the rules for lambda

is in the lambda calculus

what is left I mean we always have the this sort of rules like p ever leads to see and

q ever leads to see the c1 c2 and then the sum of course this is the same symbol here but this

symbol the plus is the this formal plus which we use to form expressions and this plus is the

plus over integers so when I write the plus on the right hand side what I mean is a really add the

integers and this is the result there are certain certain variants about how one can

interpret the logical connectivities or let's consider this junction

so if we have let's say B and waiting to true then we can say that B or C ever

leads to true this makes a certain sense because you can say if I have related a formula and you

obtain truth then you also need not evaluate the the second formula because you may have

divergence and you don't want it because you already have a truth condition so you may say

my the semantics of my conjunction as such that truth is sufficient if and even if the