+
1
|
skin
|
login
|
edit
{λ way}
::
word2talk
user:anonymous
{img {@ src="data/chevaux.jpg" width="100%" title="Mustangs at Las Colinas, Texas, @Robert Glen"}} _h1 from λ-word to λ-talk _p We have shown that the λ-calculus can be seen as a subset of {u [[λ talk|?view=lambdatalk three]]}. And conversely, that {u λ talk} can be seen itself as one of its dialects. In this page, as a demonstration, we progressively rewrite in the λ talk syntax the first basic elements of the λ calculus, the axioms: {b [variable|abstraction|application]}, and what can be built on them: {b numbers, operators, structures, ...} from which the complete set of lambdatalk's functionalities could be thoretically derived. {pre {@ style="white-space:pre-wrap"} °° _h4 1) lambda word Basically lambda-word could be defined like this: expression := word | abstraction | application 1) word is any sequence of chars except spaces and {}, -> evaluated to itself 2) abstraction is the special form {lambda {:words*} expression}, -> evaluated to the reference of an anonymous function, 3) application is a form {abstraction expression}, -> evaluated to a sequence of words For instance: 1) words Hello World -> Hello World 2) abstraction {lambda {o a} oh happy day!} °° -> {lambda {o a} oh happy day!} °° 3) application {{lambda {o a} oh happy day!} oOOOo aaAAaa} °° -> {{lambda {o a} oh happy day!} oOOOo aaAAaa} °° _h4 2) lambda word (with constants) Introducing the special form {def name expression} we can populate a dictionary with constants and give names to lambdas. {def Hi Hello World} -> Hi {Hi} -> Hello World {def good_day {lambda {o a} oh happy day!}} -> good_day {good_day oOOOo aaAAaa} -> oOOOoh haaAAaappy daaAAaay! At this point lambda word knows nothing but text substitutions. It's time to introduce numbers. _h4 3) lambda calc We define the so-called Church numbers: {def zero {lambda {:f :x} :x}} -> zero {def one {lambda {:f :x} {:f :x}}} -> one {def two {lambda {:f :x} {:f {:f :x}}}} -> two {def three {lambda {:f :x} {:f {:f {:f :x}}}}} -> three {def four {lambda {:f :x} {:f {:f {:f {:f :x}}}}}} -> four Applied to a couple of any words, we get strange things: {zero foo bar} -> bar {one foo bar} -> (foo bar) {two foo bar} -> (foo (foo bar)) {three foo bar} -> (foo (foo (foo bar))) {four foo bar} -> (foo (foo (foo (foo bar)))) We define the function church which translates Church numbers in a more familiar shape: {def church {def 1+ {lambda {:x} {+ :x 1}}} {lambda {:n} {{:n 1+} 0}}} -> church where '+' is supposed to be a primitive function written in the underlying language, so: {church zero} -> 0 {church one} -> 1 {church two} -> 2 _h4 4) a first set of operators Based on the Church numbers, we can define a first set of operators: {def succ {lambda {:n :f :x} {:f {{:n :f} :x}}}} -> succ {def add {lambda {:n :m :f :x} {{:n :f} {{:m :f} :x}}}} -> add {def mul {lambda {:n :m :f} {:m {:n :f}}}} -> mul {def power {lambda {:n :m} {:m :n}}} -> power and test: {church {succ zero}} -> 1 {church {succ one}} -> 2 {church {succ three}} -> 4 {church {add two three}} -> 5 // 2+3 {church {mul two three}} -> 6 // 2*3 {church {power three two}} -> 9 // 3^2 _h4 5) a second set of operators Building a second set of operators like "pred" or "subtract" is not obvious. Defining "pair" structures will make things more easy: {def cons {lambda {:a :b :c} {:c :a :b}}} -> cons {def car {lambda {:c} {:c {lambda {:a :b} :a}}}} -> car {def cdr {lambda {:c} {:c {lambda {:a :b} :b}}}} -> cdr {car {cons A B}} -> A {cdr {cons A B}} -> B {church {car {cons {mul two three} {succ two}}}} -> 6 {church {cdr {cons {mul two three} {succ two}}}} -> 3 {def pred {def pred.pair {lambda {:p} {cons {cdr :p} {succ {cdr :p}}}}} {lambda {:n} {car {{:n pred.pair} {cons zero zero}}}}} -> pred {church {pred zero}} -> 0 {church {pred one}} -> 0 {church {pred two}} -> 1 {church {pred three}} -> 2 {def subtract {lambda {:m :n} {{:n pred} :m}}} -> subtract {church {subtract four three}} -> 1 {church {subtract one one}} -> 0 _h4 6) iterations Now we are ready to evaluate complex expressions, like the factorial n! = 1*2*3*...*n: {def fac {def fac.pair {lambda {:p} {cons {succ {car :p}} {mul {car :p} {cdr :p}}}}} {lambda {:n} {cdr {{:n fac.pair} {cons one one}}}}} -> fac {church {fac two}} -> 2 {church {fac three}} -> 6 {church {fac four}} -> 24 {church {fac five}} -> 120 And in order to stay in the initial pure lambda calculus frame, we could even forget user defined names, "one, five, mul, succ, cons, car, cdr, fac" and evaluate a factorial like this: 6! = {{λ {:n} {{λ {:p} {:p {λ {:x :y} :y}}} {{:n {λ {:p} {{λ {:a :b :m} {{:m :a} :b}} {{λ {:n :f :x} {:f {{:n :f} :x}}} {{λ {:p} {:p {λ {:x :y} :x}}} :p}} {{λ {:n :m :f} {:m {:n :f}}} {{λ {:p} {:p {λ {:x :y} :x}}} :p} {{λ {:p} {:p {λ {:x :y} :y}}} :p}}}}} {{λ {:a :b :m} {{:m :a} :b}} {λ {:f :x} {:f :x}} {λ {:f :x} {:f :x}}}}}} {λ {:f :x} {:f {:f {:f {:f {:f {:f :x}}}}}}}} = 720 Theoretically, we could go on this way to build the majority of lambda calculus' operators, div, true, false, of, or, and, ... and even the Y-combinator which helps almost-recursive functions to be recursive. Let's remind us that we can use the power of modern browsers! _h4 7) lambda talk In order to bring a bit of humanity - and make coding much more easy - it's more reasonable to play with readable defined names and populate the dictionary with some useful primitive functions built on the browser's foundations, Javascript's numbers, Math operators and functions, HTML tags, CSS rules, and some others. With an augmented set of special forms, [lambda, def, if, let, quote, ...], all these "improvements" lead to a more usable and effective language, lambdatalk. We won't go on further in this short presentation and we will only show how the factorial function can be recursively defined and called in current lambdatalk, using two ways: 1) using nothing but 2 special forms, [lambda, quote] and a simple primitive, {when bool then one else two}: °° '{{lambda {:f :n} {:f :f :n}} {lambda {:f :n} {when {quote {= :n 1} then 1 else {* :n {:f :f {- :n 1}}}}}} 6} -> {{lambda {:f :n} {:f :f :n}} {lambda {:f :n} {when {quote {= :n 1} then 1 else {* :n {:f :f {- :n 1}}}}}} 6} °° 2) or using 3 special forms [if, lambda, def] {def fac {lambda {:n} {if {= :n 1} then 1 else {* :n {fac {- :n 1}}} }}} -> fac {fac 6} -> 720 For more informations, feel free to browse the pages of this wiki, you could begin by this one, [[overview]], and follow 'ze' lambda way. You are welcome! Alain Marty, 2016/06/24 (update on 20160819) °°} °°° {img {@ src="data/ecrire.jpg" width="100%" title="Another version of the Turing machine. (Unknown)"}} °°° {center _h4 see [[lambdacalculusWITHrecursion]]}