Lambda-Term (f x) (x f) translated to Ocaml?

Lambda-Term (f x) (x f) translated to Ocaml?

[Oliver Bandel]

Hello,

I'm not firm in lambda calculus, what is the lambda-term
in the subject translated to OCaml?

Is this possible?
And how will it be evaluated?

Any hint is welcome.

TIA,
  Oliver Bandel


P.S.: Also welcome is a "Lambda-Calculus for Dummies" recommendation
      on literature (or web-links). ;-)

Re: [Caml-list] Lambda-Term (f x) (x f) translated to Ocaml?

[Thomas Fischbacher]

> P.S.: Also welcome is a "Lambda-Calculus for Dummies" recommendation
>       on literature (or web-links). ;-)

Crash Course:

http://www.cip.physik.uni-muenchen.de/~tf/lambda/aei

And furthermore - as you are german anyway:

http://www.cip.physik.uni-muenchen.de/~tf/lambda

I would not say that this material is of sufficiently high quality to 
publish it in a book (I consider it to be only ~90% correct, for example), 
but I think it nevertheless is reasonably okay.

-- 
regards,               tf@cip.physik.uni-muenchen.de              (o_
 Thomas Fischbacher -  http://www.cip.physik.uni-muenchen.de/~tf  //\
(lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y)           V_/_
(if (= x 0) y (g g (- x 1) (* x y)))) n 1))                  (Debian GNU)

Re: [Caml-list] Lambda-Term (f x) (x f) translated to Ocaml?

[yoann padioleau]

> Hello,
> 
> I'm not firm in lambda calculus, what is the lambda-term
> in the subject translated to OCaml?
> 
> Is this possible?

the ocaml interpreter dont want this definition

let g f x = (f x) (x f)

and shout: 
  this expression has type ('a -> 'b) -> 'c -> 'd but is here used with type 'a

I guess that this is not a lambda term that can be typed.
There are many of them. A famous one is the Y combinator.
The _typed_ lambda calculus does not allow all the lambda terms
of the (normal) lambda calculus.

> 
> P.S.: Also welcome is a "Lambda-Calculus for Dummies" recommendation
>       on literature (or web-links). ;-)
> 

I liked very much:
 G.J.Michaelson, An Introduction to Functional Programming Through Lambda Calculus, Addison-Wesley
now available online from
 http://www.macs.hw.ac.uk/~greg/books.html

> 

Re: [Caml-list] Lambda-Term (f x) (x f) translated to Ocaml?

[Marius Nita]

yoann padioleau wrote:
>> Hello,
>>
>> I'm not firm in lambda calculus, what is the lambda-term
>> in the subject translated to OCaml?
>>
>> Is this possible?
> 
> the ocaml interpreter dont want this definition
> 
> let g f x = (f x) (x f)
> 
> and shout: 
>   this expression has type ('a -> 'b) -> 'c -> 'd but is here used with type 'a
> 
> I guess that this is not a lambda term that can be typed.
> There are many of them. A famous one is the Y combinator.
> The _typed_ lambda calculus does not allow all the lambda terms
> of the (normal) lambda calculus.

g can't be written, but (f x) (x f) works for suitable values for f and 
x :) Namely if f = x = id. There's probably some deep parametricity 
property at the heart of it.

-marius

Re: [Caml-list] Lambda-Term (f x) (x f) translated to Ocaml?

[Oliver Bandel]

On Tue, Mar 28, 2006 at 02:44:55AM +0200, yoann padioleau wrote:
> 
> > Hello,
> > 
> > I'm not firm in lambda calculus, what is the lambda-term
> > in the subject translated to OCaml?
> > 
> > Is this possible?
> 
> the ocaml interpreter dont want this definition
> 
> let g f x = (f x) (x f)

Oh, looks easy....  ( at least the definition on the left side ;-) )




> 
> and shout: 
>   this expression has type ('a -> 'b) -> 'c -> 'd but is here used with type 'a

OK, 
I tried this:


=====================================================================
first:~/Desktop oliver$ ocaml
        Objective Caml version 3.09.0

# let g f x = (f x) (x f) ;;
This expression has type ('a -> 'b) -> 'c -> 'd but is here used with type 'a
# ^D
first:~/Desktop oliver$ ocaml -rectypes
        Objective Caml version 3.09.0

# let g f x = (f x) (x f) ;;
val g : (('a -> 'c as 'b) -> 'c -> 'd as 'a) -> 'b -> 'd = <fun>
# 
=====================================================================

Well, looks complicated to me.

Any hints to this?

Ciao,
   Oliver

Re: [Caml-list] Lambda-Term (f x) (x f) translated to Ocaml?

[Thomas Fischbacher]

> I guess that this is not a lambda term that can be typed.
> There are many of them. A famous one is the Y combinator.
> The _typed_ lambda calculus does not allow all the lambda terms
> of the (normal) lambda calculus.

# let rec y f = f (y f);;
val y : ('a -> 'a) -> 'a = <fun>

-- 
regards,               tf@cip.physik.uni-muenchen.de              (o_
 Thomas Fischbacher -  http://www.cip.physik.uni-muenchen.de/~tf  //\
(lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y)           V_/_
(if (= x 0) y (g g (- x 1) (* x y)))) n 1))                  (Debian GNU)

Re: [Caml-list] Lambda-Term (f x) (x f) translated to Ocaml?

[yoann padioleau]

On 31 mars 06, at 23:01, Thomas Fischbacher wrote:

>
>> I guess that this is not a lambda term that can be typed.
>> There are many of them. A famous one is the Y combinator.
>> The _typed_ lambda calculus does not allow all the lambda terms
>> of the (normal) lambda calculus.
>
> # let rec y f = f (y f);;
> val y : ('a -> 'a) -> 'a = <fun>

I know that, but you cheat. This not a lambda calcul Y combinator.


>
> --  
> regards,               tf@cip.physik.uni-muenchen.de              (o_
>  Thomas Fischbacher -  http://www.cip.physik.uni-muenchen.de/~tf  //\
> (lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y)           V_/_
> (if (= x 0) y (g g (- x 1) (* x y)))) n 1))                   
> (Debian GNU)
>