Idea about how to simulate variable assignment in lambda calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I don't know if the idea might be useful for anything or maybe it's
not even new (i tried to look for it), but i would like to share it
anyways.

M,N  E  Terms  ::=   x | λx.M | M N | # M # | x := M

Reduction rules:

Beta:

(λx.M) N -> M[N/x]

Boundary Removal:

# M # -> M   (condition: If doesn't exist any variable assignment ':=' inside M)

Variable Assignment:

(λx1,x2,..,xn.# ... x:=M ... #) V1 V2 ... Vn -> (λx1,x2,..,xn. (λx.#
... I ... #) M) V1 V2 ... Vn

where  I = Identity = λx.x

x:=M becomes I and the variable x becomes binded at the boundary where
a redex is created with M as the applied term.

*** Important restriction, M should only have variables which are free
within the boundary and/or closed terms. More specifically, there

mechanized metatheory of standard ml alpha release

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Motivated by the current interest in many aspects of mechanized  
metatheory for programming languages, we are releasing an "alpha"  
version of our mechanization of the metatheory of standard ml, which  
is available from our respective publications pages.  The tarball that  
you will find there contains the formalization and verification of  
Standard ML by elaboration into an internal language, as described in  
our POPL paper with Daniel Lee.  It should be understood that this is  
an alpha release that certainly needs polishing for presentation and  
clarity, and may be revised before we go to a full publication.   
Additionally, it is also possible that it may contain errors, not that  
compromise safety, but that may depart from the intended semantics.   
We are currently validating the mechanization to rule out such  
mistakes.  We do, however, deliberately exclude some obsolete or  
deprecated features of Standard ML (notably equality types).

Thanks for your interest!
Karl Crary
Bob Harper

CPS and accumulators

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello! First of all I'd like to introduce myself: I'm Giuseppe Maggiore, MSc
student doing his thesis who has very recently found out about the wonders
of functional languages. Having always been extremely fond of computer
graphics, when I found out that there is another field at least as worthy of
my affections tore me a bit. Luckily all is well now, since I have realized
that functional languages are actually one of the best imaginable tools for
writing the extremely high parallel code that modern graphics cards (GPUs)
execute. I have realized after a bunch of long sessions with my advisor
(prof. Michele Bugliesi) that all we need is a way to generate tail
recursive code to find all those hidden dependencies between computations so
that we can map those to the same parallel processors (or if there are too
many dependencies we just don't execute the computation in parallel at all).
A CPS transform is apparently all we need, but I was wondering if there is a
more straightforward way to generate tail recursion with accumulating
parameters. Am I rambling about this last part? Can I get some more feedback
from you experts (my advisor is really great, but there isn't that many
people in our university you can discuss these topics with :D)?

thanks!
--

-- 
Giuseppe Maggiore
Microsoft Student Partner - Ca' Foscari University of Venice, Italy
B.Sc. in Computer Science
Tel. +393319040031

Re: CPS and accumulators

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Aug 19, 2009, at 2:21 AM, Giuseppe Maggiore wrote:

> ... all we need is a way to generate tail recursive code to find all  
> those hidden dependencies between computations ...

The above appears to be your central sentence. But it contains two  
distinct ideas:

  -- generate TR code, which is about code generation and the  
organization of the compiler's intermediate stages ("middle end"); and

  -- find (hidden) dependencies, which concerns the analysis of source  
code to predict the flow of values before you even run the program.

There is indeed a relationship between these two but not necessarily  
the one that your English connective phrase "to find all those" implies.

Before I send you off on a wild-goose chase, what is the real purpose  
of your project? Write the analysis component for a compiler so that  
you can ship come of the code to the GPU? Write the intermediate  
representation? (CPS? ANF? In between?) Connect the latter to the  
former? (See a paper in the upcoming ICFP on just this issue.) Or an  
entire high-performing parallelizing compiler? (Which is usually a  
project for several people over several years).

All the best -- Matthias

Re: CPS and accumulators

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Of course what you cited from my first mail was a bit hyperbolic :)

To be precise, the thesis focuses on optimizing certain pieces of code that
work on sequences. The idea is roughly to take functions that manipulate
lists and turn them into equivalent code that runs on a GPU. I will use
DirectX compute shaders called from F#, since CUDA works only on nVidia and
with Larrabee on the horizon I have no intention of being locked to the
hardware.

The idea is to avoid trying to compile entire programs on the GPU, since
that would be crazy: GPUs are SIMD machines, so there really is no point in
trying to map independent pieces of code to different cores because having
diverging instructions they would just be executed sequentially. Whenever a
sequence is processed recursively, though, there might be some hope of
recognizing it and translating the code (if it is simple enough, otherwise
it's not worth it) to the GPU, basically recognizing all those functions
that somehow "look" like map, filter, sort, etc. This approach is vastly
simpler than "writing a compiler for a GPU", but given the current state of
the hardware it also has more chances of becoming something reasonably
working (compiling an entire FL to the GPU would mostly generate slower
code).

PS: I have done quite a lot of computer vision on GPUs with a local research
group to get the hang of the process (I have done shaders since, well,
ever): the amount of time you could save by not using those awful and
unreadable GPU languages would be immense, and you would still be able to
tap into the power of the GPU even without all the fine-tuning!

Re: proofs of strong normalization for System F

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> I would like to learn about different proofs of strong
> normalization for System F and related systems (featuring
> impredicativity), and also about formalizations of such proofs.  
> In particular, I am curious if there are any proofs that depart
> significantly from Girard's original proof idea.   

Hello Andrei, sorry for the late reply.  Another way of proving
termination for System F (under the CBV reduction relation) is to
embed System F in the polymorphic pi-calculus in the following
steps.

a. Take the CBV version of Milner's translation of (untyped)
    lambda-calculus into (untyped) pi-calculus.

b. Translate System F types into polymorphic pi-calculus types.

c. Show that the translation in (a) embeds terms that are typable
    in System F as processes that are typable in the polymorphic
    pi-calculus.

d. Show that whenever a System F term M has a one-step CBV
    reduction then the translation has an n-step reduction in
    the pi-calculus for some n > 0.

e. Show that the polymorphic pi-calculus is strongly normalising.

All steps have been proven in [1], all steps but (e) are
straightforward.  Our proof of (e) is an adaptation of the usual

teaching discrete math and logic to undergraduates

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi guys,

For now three years, I have been teaching a Discrete Math course
for undergraduates. I believe that it is important to expose these kids
to logic, and since they should not be too brainwashed yet, I  try
to present a proof system in natural deduction format in order
to show them the difficulties with the "proof by contradiction  
principle"
and make them aware of some of the non-constructive aspects
of classical logic. I

  wrote some notes that I may want to convert into a book.
There is also some good stuff on combinatorics and graphs.
I have most solutions to my problems written up and more problems
should be added.
I'd be happy if you have any comments or suggestions.
You'll find the manuscript there:

http://www.cis.upenn.edu/~jean/gbooks/discmath.html

Best,
-- Jean Gallier

Re: teaching discrete math and logic to undergraduates

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Aug 21, 2009, at 5:36 PM, Jean Gallier wrote:

> For now three years, I have been teaching a Discrete Math course
> for undergraduates. I believe that it is important to expose these  
> kids
> to logic, ...

Agreed!

On this note, some three years ago NEU started teaching a
follow-up spring-semester course to Discrete Mathematics that
introduces _freshmen_ to theorem proving about code. We use ACL2,
which  nicely fits to the design discipline we teach with Scheme/"How
to  Design Programs" in the first (fall) course. In our dialect of
ACL2 students can write interactive video games in a functional
language and can them prove theorems about the actual running code.
The proof discipline matches the design discipline and prepares
students for reasoning about abstract/virtual machines.

While my graduate students and I started the course, Pete
Manolios (cc'ed) has taken over and has delivered the course
for the past two years. I am sure he can point interested parties
to relevant web pages (privately or if there's enough interest
on the list).

-- Matthias

Re: teaching discrete math and logic to undergraduates

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Thanks for sharing these excellent notes with us.  I had a quick look at 
the logic section.  I think it is worth emphasizing that a proof by 
contradiction of a *negative* statement is perfectly constructive.  In 
fact it is not a proof by contradiction usually, it just looks like it.  
You give the example of showing that sqrt(2) is irrational.  Irrational 
means rational ==> false and thus
a constructive proof of this should proceed exactly in the way you  have 
shown.  Students and professional mathematicians  over-rate the 
importance of  proof-by-contradiction as a  technique.   When do we 
really use proof by contradiction to prove a positive statement?  Fairly 
often, but not as often as is made out.   A lot of proofs by 
contradiction have this pattern:

I want to show A implies B.  So assume A and NOT-B.  Now prove B then 
exclaim, contradiction!  OK, so I was half-joking.  I am sure none of 
the readers of this group do this, but I have seen students do it.

In the example you gave of a truly non-constructive proof: there exist 
two numbers a,b such that a,b are both irrational but a^b is rational 
you can get more of a bang if you point out that there is an obvious 
constructive proof:  take a to be sqrt(2) and b to be 2 log_2 3.  Then 
a^b = (sqrt(2))^[2log_2 3] = 3.  [I found this in Lambek and Scott].
Cheers
Prakash

Jean Gallier wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>

non-constuctive proofs

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Thanks Prakash!

By the way, I  reveal the a= sqrt{2}  and b = log_2 9 trick on page  
51 of my notes!

Best,
-- Jean