G’day all :slightly_smiling_face:

where are those bagels! :stuck_out_tongue:

I like the weather so far

Not 8:30 yet!

well yes, you’re performing according to the spec so far, it’s just that we’re hungry :slightly_smiling_face:

how do you guys type all those Unicode characters in Racket? lambdas and gammas and ⊢ and so on?

In DrRacket you type the latex command and then hit the magic Unicode button. Control- on a mac if I am not mistaken

(The edit menu has a dialog with a list of key bindings to get the actual keystroke)

The docs have a list of all of them somewhere.

okay, command- gives me lambda

but I don’t know about the rest

okay, typing \Downarrow and then Ctrl- works :slightly_smiling_face:

and this is the link for any other curious people: https://docs.racket-lang.org/drracket/Keyboard_Shortcuts.html#%28part._.La.Te.X_and_.Te.X_inspired_keybindings%29

emacs’ racket-mode: C-M-y to insert lambda

Also this: https://github.com/david-christiansen/dr-racket-like-unicode

Working through the notes for this session, I noticed alpha-equivalent? requires the language to be passed in, even though default-language was called earlier in the file. Is that intentional?

Or — alternative hypothesis, does default-language only affect metafunctions under term?

it would have been good if the two functions had consistent interfaces, I agree. IIRC, alpha-equivalent predated substitute and the whole “current language” plumbing into Redex.

can you PM me the survey link here please?

https://docs.google.com/forms/d/e/1FAIpQLSeuBv6wtetyGzLh81HayvFUnA3ESKjAruIfEzyWLZozrnpEag/viewform?usp=sf_link

Thanks, @newcombj!

https://en.wikipedia.org/wiki/Programming_Computable_Functions

Our notion of PCF here is slightly different though because we have not introduced type checking.

Is it possible to see which context decomposition was used to perform a particular reduction? I’m a little confused by something I’m seeing in traces, and I’m trying to work backwards to find out what’s causing it.

@twisol : use redex-match in the REPL.

Eg:

> (redex-match Lambda (in-hole C <lhs-of-reduction>) (term <expression that is confusing>))

I’m not able to make that work; it’s giving me some errors about “in-hole’s first argument is expected to match exactly one hole”

I’m through section 1.5 in the morning lecture notes, and I’m trying to understand how e3 gets broken down and reassembled to produce ((lambda (x«13») x«13») z)

that error comes about when you have an illformed C, which might, in fact, be the real problem

Hmm, can traces or apply-reduction-relation even work with an illformed C?

Also, I’m working with code copied direct from the lecture notes

Hm. I think my original response is still correct, so perhaps you should tell me what you actually did

What I did with redex-match?

yes

> (redacted; mispaste)

> (redex-match Lambda-calculus (in-hole C e3) ((lambda (x«13») x«13») z))
. . z: undefined;
 cannot reference an identifier before its definition

> (redex-match Lambda-calculus (in-hole e3 e) ((lambda (x«13») x«13») z))
. redex-match: in-hole's first argument is expected to match exactly one hole, but it cannot match a hole in: (in-hole e3 e)

Oops

first one was a mispaste

The second argument (the one after the language) needs to be a pattern

The e3 isn’t that

That’s what that error message mens

means

Aah. (term ,e3)?

no

Put hte left-hand sside of the reduction rule that you’re interesting in where e3 appears

try: (redex-match Lambda-calculus (in-hole C ((lambda (x) e_1) e_2)) e3)

Oh, by “expression that is confusing” I thought you meant the result I had called confusing.

You meant the input.

If anyone else got confused by this: in the definition of ->beta in the lecture notes, it looks like the arguments to substitute are flipped. It reads (in-hole C (substitute e_2 x e_1)) but it should be (in-hole C (substitute e_1 x e_2)).

Thanks to the TA who helped me figure this out!

I just finished #8 \o/

Were the reimbursement forms handled already in the morning, or has that not happened yet? (I came in a little late…)

Where is everyone getting food? The student Union is closed…

Oh no talk of reimbursement yet @twisol

I’m curious how anyone else approached #8. It seems like something you could reasonably arrive at a few different solutions for.

oh, maybe this should be a subthread to avoid spoilers

o/

it seems like the function from #6 was intended to be helpful, perhaps

Yeah, I did end up using lookup

I wrote an increment-env helper to add 1 to every expression in an environment, and used that whenever recursing under a lambda

i got one solution, but I thought of a different way that I’m going to try that avoids having to update everything in the environment all the time

yes, that’s the same approach I took.

but it feels very inefficient, though it works

Cool! Ah, I wonder if you could do a lookup and push an incremented count when going under a lambda?

Er, not incremented, zero’d

I think you can do better… :slightly_smiling_face:

Wait, that’s mostly totally useless…

Are you thinking of something like a zipper?

no… but increment a depth count and carry it along with the environment; then only push the count value with the variable when going under a lambda… when you actually hit a variable, you then do a lookup, but you have to adjust the actual value using the depth count…

Hmm, I see.

I was thinking of something like, (1) push a variable whenever you go under a lambda, and (2) count the number of variables before the first occurrence of a particular variable

by ‘before’ you mean in the environment?

Yes

so (z x y x) would correspond to ((x 1) (y 2) (z 0))

oh - so you don’t need an environment at all then? just a stack of variables and ability to count how far down in the stack a variable is

Right, I think so. Which makes sense — that’s kind of what “scope” is, in some sense.

There’s much less work to do when moving under a lambda, although you have to do more work when looking a variable up. And it’s more of a purely-functional data structure.

probably not, because you had to do a lookup anyway to find the variable in the environment, and it would be just as far down in the environment as it is in the stack, so same number of ops

oh, good point. I was thinking of the current env as a direct lookup table.

@newcombj The Heritage center dining hall closes at 7pm, but I think there is a store with snacks there open till 8pm, and there’s https://new.dineoncampus.com/utah/lassonde-studios

wherever that is

Thanks @nadeem ! I’ll check out the lassonde tung next time

Um… is #4 really just a 1 word change or am I misunderstanding the scope of the change?

I reused the error state from the previous exercise, but… that 1-word change does seem more straightforward.

kk. as long as I’m on the right page. thanks

Anyone seen this: define-metafunction: expected the same name in both positions ?

Yeah — it’s possible you named it one thing, but aren’t using the same name in the pattern matching position

If the signature is foo : n -> n, the clauses should look like e.g. [(foo n) n]

derp… yup.

@mflatt/@robby exercise 7 typo: (lambda (b a)) -> (lambda (b) a) — down in the term substitute code block

Probably left-over from when it was a multi-def let

(Which is a fun exercise once you complete 7, fwiw. Making it capture-avoiding is even better ^_^)

I assume you can do multiple let via recursion?

At the metafunction level, yes.

hrm… you can’t just do a rewrite only version recursively?

Metafunctions are essentially macro rewrite rules

sure

You don’t need quote/unquote/term though.

It was quite frustrating when I tried to write it without metafunction recursion.

I just did 4–7 w/o too much trouble (other than my own blindness, thank you)… but 8? I don’t think I even understand the problem definition… static distance?

I wrote some nasty stuff with foldr, but couldn’t get it to work.

zenspider, does the term “de Bruijn indices” help?

heh. nope

@twisol The answer to that question is probably universally no. :wink:

did I gloss over some reading?

@awe I’ve spoken with several people over the last few weeks who know about that. It’s just a very brief way to explain it if someone already knows it.

Stepping backwards…

Take (lambda (x) (lambda (y) (x y))) as an example.

That should be replaced with (lambda (x) (lambda (y) ((sd 1) (sd 0))))

the lambda binding y is 0 distance “up”

the lambda binding x is 1 distance “up”

@nadeem has some test cases you could use to develop against, but I don’t want to redistribute them without permission

so this is like the variable rewriter x«0»

No, that notation is utilized internally to Redex to generate fresh variable names

lemme give a better example

minor change: (lambda (x) (x (lambda (y) (x y)))).

becomes: (lambda (x) ((sd 0) (lambda (y) ((sd 1) (sd 0)))))

in this case, x is changed to two different things

so… this isn’t used for something like hygiene?… then… stack lookup?

Stack lookup is basically exactly what it is.

hrm: “Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality.”

You’re referring to the de Bruijn page?

α-equivalence is just hygiene (gah I can NEVER spell that right), no?

yeah

In a certain sense, hygiene (me either) is about preserving alpha-equivalence under substitution.

Put it this way. Put a bunch of your friends in a line. You’ve got Alice, Bob, Mary, and Sue.

I hate them all so much

and that’s 20 years later… I still hate them

If you ask Bob and Sue how far away Alice is, you’ll get different answers: 1 and 3.

This is effectively what “static distance” is trying to capture. Different places referring to the same variable will be different distances away.

(lambda (alice) (lambda (bob) (alice (lambda (mary) (lambda (sue) alice)))))

kk. got it. thanks.

np, hope it helps!

not sure I can muster a fuck to give at this point… I’m so beat… but I can at least write some failing tests.

@twisol since you’re up…

Did you understand MF’s answer to my question about wrapping expected test values in (term ...)?

Because I didn’t… the javascript bit threw me… afaict, term is basically just an unquote (more than that, but sorta kinda)… is there some translation layer it goes through if I had to change the internal representation of the values?

I don’t see that answer in chat history — was this in person?

yeah. sorry. in the room today. He was writing tests and doing (test--> ->value (term input...) (term expected...))

when the expected could be tested with just '(1 + 1) and the like

his answer was about when you’re implementing a language like javascript and you can’t just piggyback on racket’s number system

but I don’t see how (term 42) would work as an expected w/ a different number system unless there’s some translation layer

I don’t fully (read: almost at all) understand what goes on under the hood in Redex, but there’s some conflation of domains when you’re working with primitive values.

I’m pretty sure (term 42) is just 42

right… and that was the gist of the answer… and why I’m confused :slightly_smiling_face:

Well, so, if addition in your language is different from addition in your host language, you can’t just write a non-term expression in the expected value, since you’re doing different operations.

There’s an example of that on the third lecture notes page, http://www.ccs.neu.edu/home/matthias/summer-school/mon-aft.html

4 is 4… unless the internal representation is different

@twisol you can post those test cases (I’m not sure I know how to paste code snippets here)

@nadeem, hit the + to the left of the message area and select “code snippet”

but maybe put it as a reply to someone in case of spoilers

or type 3 backticks, paste, 3 backticks (or their own line) and hit return

That kind of code block doesn’t collapse down, unfortunately

snippets can be super long without impinging too much on the chat field

sure

ok, here’s a thread with a few test cases for #8 as hints

;; tests
(test-equal (term (sd* z)) (term z))
(test-equal (term (sd* (λ(x) y)))
            (term (λ(x) y)))
(test-equal (term (sd* (λ(x) x)))
            (term (λ(x) (sd 0))))
(test-equal (term (sd* (λ(x) (λ(y) x))))
            (term (λ(x) (λ(y) (sd 1)))))
(test-equal (term (sd* (λ (x) (λ (y) y))))
            (term (λ(x) (λ(y) (sd 0)))))
(test-equal (term (sd* (λ(z) ((λ(y) (y (λ(x) x))) (λ(x) (z x)))) ))
            (term      (λ(z) ((λ(y) ((sd 0) (λ(x) (sd 0)))) (λ(x) ((sd 1) (sd 0)))))))

(define left-term     (term (λ(a) ((λ(b)(b a))
                                   (λ(c) (λ(a) (a (c b))))))))
(define right-term    (term (λ(b) (b (λ(c) (λ(d) (d b)))))))

(define left-term/sd  (term (λ(a) ((λ(b)((sd 0) (sd 1)))
                                   (λ(c) (λ(a) ((sd 0) ((sd 1) b))))))))
(define right-term/sd (term (λ(b) ((sd 0) (λ(c) (λ(d) ((sd 0) (sd 2))))))))

(test-equal (term (sd* (,left-term ,right-term)))
            (term (,left-term/sd ,right-term/sd)))

aww, it’s a shame snippets don’t work under threads.

yeah

cool. thanks @nadeem and @twisol

In these, I assumed that free variables (not bound by a lambda) remain unaffected.

the book doesn’t clarify my term q at all

@zenspider: as far as I can tell, term ensures that metafunctions are expanded. If you didn’t use term you might produce a syntax tree with syntax not expected by the object language

it’s probably good to use term habitually when dealing with object language constructions, to keep the host/object boundary fairly distinct

what was your term question?

@nadeem starts here https://racket.slack.com/archives/C5T5RQ546/p1499747890445332

ugh. I hope that works internally

seems to!

HAH! run (render-language PCF) in your repl

I love that that even works in emacs

yeah, I don’t think term does any special conversions to values. I think it’s just a quote customized for constructing syntax trees, and if you don’t need metafunctions, it’s probably practically equivalent to quote.

cool, even better (render-metafunctions sd* sd-help)

oooooo

hah. with escaped racket code in bright pink

yes, I’ve been just reading term mostly as quote, so it seems to me you’d need do something like (term (js 42)) in the modeling javascript situation, where js is some metafunction that translates the racket representation of 42 to a proper javascript model of the number

Do note this page though, where you can see all the things you can inject into your language: http://docs.racket-lang.org/redex/The_Redex_Reference.html#%28part._.Patterns%29

of course, I don’t know whether Racket uses IEEE double-precision floats, but if it does, number might be sufficient…

(I wonder what the difference between number and real is? It isn’t specified.)

(Maybe complex numbers. http://docs.racket-lang.org/reference/numbers.html)

http://docs.racket-lang.org/reference/numbers.html?q=real%3F#%28tech._real._number%29

http://docs.racket-lang.org/reference/number-types.html?q=real%3F#%28def._%28%28quote._~23~25kernel%29._real~3f%29%29 helps too

ok.. my brain is melted. thanks all.

and I still have 23% battery for today… damn

electronic battery technology has surpassed human battery technology