[Next]  [Previous]  [Up]  

Problem # 24

Submitted by Corrado Böhm
Date: 2013
Statement. On the equational meaning of deeds
Problem Origin. The problem has been posed first by Corrado Böhm . It is added to the list to celebrate his 90th birthday.


A deed is a closed normal form with only one initial abstraction, namely a deed has shape λx.xP  ...P
     1     n  where n ≥ 0  .

It is easy to verify that each equation of the shape

D1X   = D2X,

where D1   , D2   are deeds, can be solved, for instance by choosing a fixed point of the combinator K  as X  .

It it possible to define a one-one mapping between arbitrary normal forms and deeds, as follows. Given a normal form M  with m  ≥ 0  initial abstractions, the deed corresponding to M  is:

DM   ≡ λx.M  (xc1)...(xcm),
where c1,...,cm  are the Church numerals or any distinct closed beta-eta normal forms. Note that the mapping is injective by Böhm’s theorem.

The question is as follows: What can we understand about the solution of the equation M  X =  N X  , where M, N  are arbitrary normal forms, by looking at the equation   M        N
D   X  = D  X  ?

References for # 24

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014