1

One may represent λ-terms in the λ-calculus using the following data type:

data LTerm a = Var a | App (LTerm a) (LTerm a) | Abs a (LTerm a)

Describe the encoding of the constructors, the fold, the map and the case for this datatype.

The way I encoded constructors are:

Var x := λabc.ax
App t1 t2 := λabc.b (t1 abc) (t2 abc)
Abs x t := λabc.cx(t abc)
fold a b c d = d a b c

Can you help me to understand how to implement the map and the case in λ-calculus?

An example for map and case is the List datatype:

Nil = λnc.n
Cons a l = λnc.ca(lnc)
FoldList vgl = lvg
MapList f l = FoldList Nil (λaz.Cons (f a)z) l

$$ \text{case } l \text{ of} \begin{cases} \mathsf{Nil} \mapsto t_1 \\ \mathsf{Cons} \ a \ as \mapsto t_2 \end{cases} := \mathsf{CaseList} \ l \ t_1 \ (\lambda \ a \ as . t_2) $$

$$ \mathsf{CaseList} \ l \ t \ f := \pi_1 \left ( \mathsf{FoldList} \ \langle \mathsf{Nil}, \ t \rangle \ (\lambda \ a \ \langle l, \_ \rangle . \langle \mathsf{Cons} \ a \ l, \ f \ a \ l \rangle ) \ l \right ) $$

Thank you in advance.

HallaSurvivor
  • 38,115
  • 4
  • 46
  • 87
Zhijie Xia
  • 11
  • Welcome to mse! I've edited your question to use mathjax (which is searchable) rather than an image (which isn't) so that other users will have an easier time finding this question. In the future you should do the same ^_^. – HallaSurvivor Apr 19 '23 at 03:20

0 Answers0