[FOM] Bohm trees/lambda calculus

[pax0 at seznam.cz]

Dear All, in lambda calculus:
why
 ~=
 defined by Barendregt as
 M ~= N iff BT(M)=BT(N)
 preserves solvability?

BT are Bohm trees.

Solvability of term M is this property

there is n,there exist terms N_1,...,N_n such that


MN_1...N_n=I.

If M is not closed, solvability of M means


lambda x.M, where x=FV(M).

Thank you, Jan Pax
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130308/ee35b11e/attachment.html>