-
Notifications
You must be signed in to change notification settings - Fork 17
Home
Welcome to the pLam wiki! (Work in progress...)
This home page serves as a reference to all other content related to pLam language and λ-calculus. The content described in these wiki pages deals not just with the documentation of pLam's syntax and semantics, but also serves as a mild introduction to λ-calculus and computability, along with most important definitions and results, pointing to links for further reading.
λ-variable is required to be lowercase and a single letter. For example, x is a good λ-variable for pLam and X, var,... are not. There are also environment variables (names for defined λ-expressions) which are every string that is not parsed as λ-variable, λ-abstraction or λ-application.
λ-abstraction is written the same as in the language of pure (untyped) λ-calculus, except that pLam treats a symbol \ as λ and it is required to write a space after .. For example, λx.λy.x would be written \x. \y. x in pLam. One can also write λ-abstraction in the curried form: \xy. x or \x y. x.
λ-application is written like 2 λ-expressions separated by a space, for example (\x. x) (\xy.x) or (\x. x) MyExpression or myexp1 myexp2. Brackets ( and ) are used as usual and are not required to be written; the association is to the left, so M N P is parsed as (M N) P and one needs to specify with brackets if the intended expression should be M (N P).
A block of code in pLam is a line, and possible lines (commands) are the following:
- syntax:
<string> = <λ-expression> - semantics: let the
<string>be a name for<λ-expression>. - examples:
T = \x y. x,myexpression = T (T (\x. x) T) T - restriction:
<string>needs to be of length>1 or starting with uppercase letter
- syntax:
<λ-expression>or:d <λ-expression> - semantics: reduce the
<λ-expression>to β-normal form. If:dis put in front of expression, all the reduction steps will be shown (manually or automatic, depends on what one chooses when asked) - example:
\x y. x,:d T (T (\x. x) T) T - restriction: none
- syntax:
:import <string> - semantics: put all the expressions defined in the file
import/<string>.plaminto the list of environment variables. - example:
:import std - restriction:
<string>.plamhas to be insideimport/directory within the pLam project directory
- syntax:
--<string> - semantics: a comment line
- example:
-- this is a comment - restriction: none
- syntax:
:run <string> - semantics: runs a
.plamfile with relative path<string>.plam - example:
:run <relative-path-to-plam>/examples/2.5.2 - restrictions:
~for home does not work
- syntax:
:print <string> - semantics: prints
<string>to a new line. It mostly makes sense to use it in .plam programs to be executed, not in interactive mode where a comment should do the job better. - example:
:print this is a message - restrictions: none