Arbitrarily Typed Traces in the Lambda-Calculator – And How To Bind Them
I find myself (relatively) often in a situation where I need to have arbitrarily typed traces in the Lambda-Calculator – which supports them without any problems. However, it is not easy to find the information on how to do this on the Homepage.
By default, a trace in the Lambda-Calculator is of type e, and it can be written as t_i, where i is some integer. In order to bind that trace, one simply uses i again. However, what can you do if, for some reason, you need a trace of type i or v? There is a solution.
One can simply indicate the type in the trace signature: instead of writing simply t_1, one can write t_<i>1 if one needs a trace of type i. The general recipe is therefore to write t_<TYPE>i, where TYPE is some type in the standard notation, and i again some integer.
This is how it can be done (just copy the content below into a file, and open it with the Lambda-Calculator):
ARBITRARY TYPES IN TRACES AND BINDERS
# Author: Gerhard Schaden (gerhard.schaden@univ-lille.fr),
# based on a file by Lucas Champollion (champollion@nyu.edu)
# This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License (CC BY-SA 4.0).
# You are free to share — copy and redistribute the material in any medium or format;
# adapt — remix, transform, and build upon the material for any purpose, even commercially.
# The copyright to the work of the authors cited here remains with them.
# The following directive instructs the program to
# interpret multiple-letter constants and variables
# properly.
multiple letter identifiers
# "use rule" directives are for tree evaluation exercises.
# They indicate which composition rules are available
# at nonterminals.
use rule function application
use rule non-branching nodes
use rule lambda abstraction
####################################################################################################
# Defining types
#individual entities:
variables of type e: x
# intervals, times:
variables of type i: i
variables of type <e,t>: P
constants of type <e,t>: man
constants of type <<e,t>,<<e,t>,t>>: every
constants of type <i,<i,t>>: before
####################################################################################################
# Defining a rudimentary lexicon:
define before: Li.Li'.[before(i')(i)]
define every: LP'.LP.Ax.[P'(x)->P(x)]
define man: Lx.man(x)
###################################################################################################
exercise tree
title How to introduce and bind traces of type e
instructions A trace without any indication is taken to be a trace of type e.\\
instructions A trace is written as follows:\\
instructions t_i\\
instructions where i is some integer\\
instructions In order to bind the trace, use the integer.\\
instructions \\
instructions This is only to be taken as an illustration how to do binding and traces.\\
instructions The following is a very silly example, like all the rest;\\
instructions the only aim here is to bind as fast as possible.
[ 1 [ man t_1] ]
####################################################################################################
title How to introduce and bind traces of some other (simple) type
instructions In order to specify the type of a trace, write
instructions \\
instructions t_<TYPE>i\\
instructions where TYPE is the type you want to give the trace, and i is some integer\\
instructions Assuming you want a variable of type i, you need to write\\
instructions t_<i>2\\
instructions Binders will take care of themselves
[ 1 [ 2 [ t_<i>2 [ before t_<i>1 ] ] ] ]
####################################################################################################
title How to introduce and bind traces of arbitrary complex types
instructions BECAUSE WE CAN!\\
instructions \\
instructions As before, in order to specify the type of a trace, write
instructions t_<TYPE>i\\
instructions where TYPE is the type you want to give the trace, and i is some integer\\
instructions We are being unreasonable, and for some reason, we want to make a trace of type <e,t>\\
instructions Therefore, we can write this as\\
instructions t_<e,t>7\\
instructions Binders will take care of themselves
[ 7 [every t_<e,t>7 ] ]
####################################################################################################
# EOF