From leavens@larch.cs.iastate.edu Thu Sep 23 23:12:14 2004 Date: Thu, 23 Sep 2004 23:12:14 -0500 (CDT) From: Gary T. Leavens To: Neeraj Khanolkar Subject: Re: grammar limitations? Hi Neeraj, On Thu, 23 Sep 2004, Neeraj Khanolkar wrote: > > Hi Gary, > > The \ calculus grammar does not prevent expressions where the formal > parameter is repeated. For eg: \x:o.\x:o.z, i guess this would be OK here. That's right. But this is more like: { int x; { int x; ... } } since each new lambda introduces a new scope. > But for languages such as C, is it possible to specify in the > grammar that a variable once declared cannot be declared in the same scope > again? Or does this have to be checked by the lexer using the symbol > table? No, this has to be part of the type checking (it's not context-free). This wouldn't normally be done by a lexer. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ------------------------------------------- From leavens@larch.cs.iastate.edu Fri Sep 24 15:42:25 2004 Date: Fri, 24 Sep 2004 15:42:25 -0500 (CDT) From: Gary T. Leavens To: Neeraj Khanolkar Subject: Re: Com S 541 homework 2, Parser + lexer question Hi Neeraj, On Fri, 24 Sep 2004, Neeraj Khanolkar wrote: > For the problem concerning the implementation of the infer function: > > I was planning on simply going function by function through all 3 of > the files you have provided. But decided to take the 'lazy' approach and > instead ask you- What are the most important parts that I need to > look at- and perhaps use? I would completely ignore LexerTools and ParserFunctions; you don't need to understand them at all. You can just work from the abstract syntax, which is the LambdaTerm datatype in TypedLambdaCalculus.lhs. This is quite similar to the problem with type checking for expressions with Sub etc. in homework 1. To test interactively, you can use the grammar at the bottom of TypedLambdaCalculus.lhs, which tells you what the input grammar read by the read_type_print function is. This is essentailly expr ::= Id | ( expr expr ) | ( \ Id : typeexp . expr ) typeexp ::= o | ( o -> o ) Note that the parentheses are required. See the file for details. But you can also just test based on the abstract syntax. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 -------------------------------------------------- From leavens@larch.cs.iastate.edu Sun Sep 26 12:10:46 2004 Date: Sun, 26 Sep 2004 12:10:45 -0500 (CDT) From: Gary T. Leavens To: Daniel Patanroi Subject: Re: cs541 hw 2 HI Daniel, On Sun, 26 Sep 2004, Daniel Patanroi wrote: > For part Untype lambda calculus, > I try to do type checking for I,K,S,B. > It seems no matter what type I assign to x,y,z, the type for B does > not match up. For the part of the homework on the untyped lambda calculus, you should erase all the typing from the equational rules and don't try to do any type checking on such terms as appear in these problems. If you are interested in the typing of such terms, you might want to look at problem number 3. > My question, for doing #5, should we just ignore the types? Yes. > for example > > (\y. x) (\y. x) ==> beta x > > Substituting (\y. x) for y does not make any sense to me. > Is this okay for reduction question? Yes, in this example there are no occurrences of the bound variable, y, and so that is correct. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 --------------------------- From leavens@larch.cs.iastate.edu Sun Sep 26 12:18:21 2004 Date: Sun, 26 Sep 2004 12:18:21 -0500 (CDT) From: Gary T. Leavens To: Daniel Patanroi Subject: Re: cs541 hw2 Hi Dan, On Sun, 26 Sep 2004, Daniel Patanroi wrote: > For #6, is it enough to prove by giving an example such that (A B) C > =/= A (B C) ? > Or do you want a formal proof? To prove that a (universally quantified) formula does not hold, it does suffice, even formally, to give a counterexample. In other words, if we're trying to disprove that for all the terms, A, B, and C: (A B) C == A (B C) this is equivalent to proving that it is not the case that for all the terms, A, B, and C: (A B) C == A (B C) and this is equivalent to proving that for some terms, A, B, and C: (A B) C =/= A (B C) and it's clear that the latter, admits of a proof where you simply exhibit the three terms in question. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ---------------------------------------- From leavens@larch.cs.iastate.edu Sun Sep 26 15:59:12 2004 Date: Sun, 26 Sep 2004 15:59:12 -0500 (CDT) From: Gary T. Leavens To: Raul Piaggio Subject: Re: Questions about HW 2 Hi Raul, On Sun, 26 Sep 2004, Raul Piaggio wrote: > I have some questions about some of the problems: > > Ex. 3: > > Do we have to present a formal derivation of the whole formula, as in the > previous 2 exercises, or just analyzing the point where it gets problematic > suffices? Just explain it clearly. > Ex. 4: > > I have my doubts I'm doing things right here. I never have the need to apply > the reflexive or the transitive rule. Just 2 beta applications. Am I missing > something? If you use two beta applications, then you're implicitly using the transitive closure. It's fine to not use the reflexive part; that would only be needed if the two terms were equivalent already. So it's true I could have stated this problem using only the transitive closure. > Ex. 5: > > Can we write down the result of a beta-rule application as it looks after > the substitution or should we present the intermediate step with the > explicit substitution? You don't need to present to the intermediate step with the explicit substitution; it's not usually necessary to write this out explicitly. > Ex. 9: > > If we provide an expression with free variables (therefore, the type is > unspecified), is it OK if we return Nothing? This question arises because we > could still apply beta and eta rules without knowing the type of some free > variables. Or should we report: "type check fails but we can still get this > normal form: ..."? Usually, if the type checking doesn't succeed, you wouldn't report any results. For example, this is what Haskell does. So I think it's perfectly fine to return Nothing in this case. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 -------------------------------- From leavens@larch.cs.iastate.edu Sun Sep 26 16:05:42 2004 Date: Sun, 26 Sep 2004 16:05:42 -0500 (CDT) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: COMS 541: The full type frame translated to Haskell (attached) Hi Ru He, On Sun, 26 Sep 2004 rhe@cs.iastate.edu wrote: > Could you be kind enough to answer my following question: > > Is the code in your SimplyATypedModel is complete? I think it covers the entire grammar, and thus is complete. > Especially, for the following segment of code: > >> eval (Lambda x _ e) eta = (Fun f) >> where f y = eval e eta' >> where eta' = overlay (bind x y) eta > > When I compare it with my notes, I find that the notes have more conditions in > the *where* part for eata prime. Does the code exactly match the notes? It doesn't have the same form as the notes, because in the notes, I wrote: [[H |> (\x:s.e) : s->t]]eta = f where f(y) = [[H[x:->s] |> e:t ]]eta' and eta' is an H,x:s-envirionment such that eta'(x) = y and eta'(z) = eta(z) if not(z == x) and this defined eta' by cases. But it has the same effect, because I'm using overlay explicitly to bind x to the argument to f. So it's expressed differently. Thus it doesn't exactly matched the notes. However, I couldn't get the Haskell code to exactly match the notes, because if I had written what was in the notes, I would have not used the same representation for environments as I was using in the rest of the program. Probably the simplest thing to do is to change the notes :-) Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 -------------------------------- From leavens@larch.cs.iastate.edu Sun Sep 26 16:50:22 2004 Date: Sun, 26 Sep 2004 16:50:22 -0500 (CDT) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: COMS 541: The full type frame translated to Haskell Hi Ru, On Sun, 26 Sep 2004 rhe@cs.iastate.edu wrote: > Hi, Professor: > > Thank you for your quick reply. I think that concrete/abstract syntx issue is > related to parsing, right? Could you give some other sample test input of > SimplyTypedModel for the abstration and application? Here are some more examples SimplyTypedModel> read_eval_print lambda-term? one one 1 lambda-term? x x 24 lambda-term? ((\x:o.x) one) ((\x:o.x) one) 1 lambda-term? (((\x:o.(\y:o.x)) ((\x:o.x) one)) x) (((\x:o.(\y:o.x)) ((\x:o.x) one)) x) 1 lambda-term? > Quoting "Gary T. Leavens" : > >> Hi Ru He, >> >> On Sun, 26 Sep 2004 rhe@cs.iastate.edu wrote: >> >>> Hi, Professor: >>> >>> When I tried to test SimplyTypedModel, I receive the following error when >> I >>> input some term. (see the following.) Could yo tell me what is wrong with >> my >>> input term? >>> >>> Regards, >>> >>> Ru He >>> >>> SimplyTypedModel> read_eval_print >>> lambda-term? Varref "one" >>> >>> Program error: Prelude.read: no parse >> >> You entered abstract syntax, but it wants concrete syntx. Try >> entering just "one" (with no quotes). Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 --------------------------------------------- From leavens@larch.cs.iastate.edu Sun Sep 26 20:18:07 2004 Date: Sun, 26 Sep 2004 20:18:07 -0500 (CDT) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: COMS 541: The full type frame translated to Haskell Hi Ru, On Sun, 26 Sep 2004 rhe@cs.iastate.edu wrote: > Thank you for your quick response. No problem. > Could you tell me whether I could ask you questions tomorrow morning (after > 10:00am)? I need to prepare for 362 then, so can it wait until afternoon? 2 or 4pm works. > Here, I also want to ask one question ahead of time. > > In your lecture 9, you give the following: > > (\f:o->o.\y:o.f y) (\y:o.y) > ==> beta rule > = [(\y:o.y)/f](\y:o.f y) > ==>alpha rule > = [(\y:o.y)/f](\y':o.f y') > ==> substition rule (5) since y' \= f and y' is not a element of Fv( (\y:o.y) > ) > = \y':o.(\y:o.y) y' > > In your answer, you do the alpha rule first to distinguish two y's. Right. > I want to ask wheter I could not change y to y'. I directly get \y:o.(\y:o.y) > y. > Is it still the completely correct answer though it has no clear apperance? Right, this is okay, as y is not free in (\y:o.y). I usually do a change of variables just to be safe, but in this case there was no need. > I ask this question because I want to know whether > > y \= f and y is not a element of Fv( (\y:o.y) ) > > is the sufficient condition for using substition rule (5). It is sufficient, so you are right. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ----------------------------------