Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-10-05 20:07:27 +03:00
Code Issues Projects Releases Wiki Activity

Update links

Victor Maia 2019-06-29 18:50:43 -03:00
parent c545180dfe
commit 1c6ebc94df
17 changed files with 18 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Bounded-Loops-and-Recursion.md

@ -61,4 +61,4 @@ def main:
Here, `Node` and `Leaf` are Scott-Encoded constructors, and `FNode` and `FLeaf` are Church-Encoded constructors, as defined on the last section. Notice how `tree_fold` needed to know the size of the input tree (`7`). This is because the Church-Encoded Nat `7` is used to unroll `func` up to a depth of `7`, essentially emulating a recursive function with a bounded number of iterations. With this technique, arbitrary recursive functions can be defined, as long as you put a "gas limit" on how much work they can perform. Here, `Node` and `Leaf` are Scott-Encoded constructors, and `FNode` and `FLeaf` are Church-Encoded constructors, as defined on the last section. Notice how `tree_fold` needed to know the size of the input tree (`7`). This is because the Church-Encoded Nat `7` is used to unroll `func` up to a depth of `7`, essentially emulating a recursive function with a bounded number of iterations. With this technique, arbitrary recursive functions can be defined, as long as you put a "gas limit" on how much work they can perform.
[< Datatypes](https://github.com/moonad/Formality-JavaScript/wiki/Datatypes) | [Undefined Behaviour >](https://github.com/moonad/Formality-JavaScript/wiki/Undefined-Behavior) [< Datatypes](https://github.com/moonad/Formality/wiki/Datatypes) | [Undefined Behaviour >](https://github.com/moonad/Formality/wiki/Undefined-Behavior)

2
Datatypes.md

@ -142,4 +142,4 @@ def main:
Notice how, unlike on the Scott-Encoded versions, here we are able to fold over the structures, summing all their contained values. Moreover, due to the use of boxes, elements contained by a Church-Encoded structure must always be one layer above than them, which, by consequence, means that results of folds are one layer above too. Notice how, unlike on the Scott-Encoded versions, here we are able to fold over the structures, summing all their contained values. Moreover, due to the use of boxes, elements contained by a Church-Encoded structure must always be one layer above than them, which, by consequence, means that results of folds are one layer above too.
[< Lambdas and Affinity](https://github.com/moonad/Formality-JavaScript/wiki/Lambdas-and-Affinity) | [Bounded Loops and Recursion >](https://github.com/moonad/Formality-JavaScript/wiki/Bounded-Loops-and-Recursion) [< Lambdas and Affinity](https://github.com/moonad/Formality/wiki/Lambdas-and-Affinity) | [Bounded Loops and Recursion >](https://github.com/moonad/Formality/wiki/Bounded-Loops-and-Recursion)

2
Dups-and-Boxes.md

@ -136,4 +136,4 @@ Because, once again, each occurrence of `num` is on `layer 1`. This means you're
The stratification condition is what allows Formality-Core to be evaluated by the fastest interaction-net reduction algorithm known, dispensing the expensive "bookkeeping mechanism" used by other optimal evaluators. The stratification condition is what allows Formality-Core to be evaluated by the fastest interaction-net reduction algorithm known, dispensing the expensive "bookkeeping mechanism" used by other optimal evaluators.
[< If and Cpy](https://github.com/moonad/Formality-JavaScript/wiki/If-and-Cpy) | [Lambdas and Affinity >](https://github.com/moonad/Formality-JavaScript/wiki/Lambdas-and-Affinity) [< If and Cpy](https://github.com/moonad/Formality/wiki/If-and-Cpy) | [Lambdas and Affinity >](https://github.com/moonad/Formality/wiki/Lambdas-and-Affinity)

2
Hello,-world!.md

@ -7,4 +7,4 @@ def main:
Save this as `main.fmc` and using the terminal, go to the directory where you saved the file, then run it with `fmc main`. If you see `"Hello, world!"` in your terminal, then it worked. You can also enter just `fmc` for a list of options. We support multiple evaluators, including an interpreter, lazy/strict interaction-nets and even native JS closures, all with different characteristics. Save this as `main.fmc` and using the terminal, go to the directory where you saved the file, then run it with `fmc main`. If you see `"Hello, world!"` in your terminal, then it worked. You can also enter just `fmc` for a list of options. We support multiple evaluators, including an interpreter, lazy/strict interaction-nets and even native JS closures, all with different characteristics.
[< Installation](https://github.com/moonad/Formality-JavaScript/wiki/Installation) | [Numbers and Operators >](https://github.com/moonad/Formality-JavaScript/wiki/Numbers-and-Operators) [< Installation](https://github.com/moonad/Formality/wiki/Installation) | [Numbers and Operators >](https://github.com/moonad/Formality/wiki/Numbers-and-Operators)

2
Home.md

@ -20,4 +20,4 @@ Here is an brief illustration of the process of compiling a Formality-Core term
![FM Interaction Net](https://github.com/moonad/Elementary-Affine-Net-Render/blob/master/nasic-render.gif) ![FM Interaction Net](https://github.com/moonad/Elementary-Affine-Net-Render/blob/master/nasic-render.gif)
[Installation >](https://github.com/moonad/Formality-JavaScript/wiki/Installation) [Installation >](https://github.com/moonad/Formality/wiki/Installation)

2
If-and-Cpy.md

@ -40,4 +40,4 @@ def main:
The program above outputs `[42, 84]`. This primitive is necessary because, in Formality-Core, any fixed-size data structure can be natively copied without "boxes" (which will be explained next), with the only exception being native numbers. This primitive fixes this, allowing numbers to be copied without boxes. The program above outputs `[42, 84]`. This primitive is necessary because, in Formality-Core, any fixed-size data structure can be natively copied without "boxes" (which will be explained next), with the only exception being native numbers. This primitive fixes this, allowing numbers to be copied without boxes.
[< Lets and Defs](https://github.com/moonad/Formality-JavaScript/wiki/Lets-and-Defs) | [Dups and Boxes >](https://github.com/moonad/Formality-JavaScript/wiki/Dups-and-Boxes) [< Lets and Defs](https://github.com/moonad/Formality/wiki/Lets-and-Defs) | [Dups and Boxes >](https://github.com/moonad/Formality/wiki/Dups-and-Boxes)

4
Installation.md

@ -10,8 +10,8 @@ This should install it. In order to test if it worked, type:
fmc fmc
``` ```
If you see our command-line instructions, Formality-Core has been successfully installed in your system. If you have any problem during this process, please [open an issue](https://github.com/moonad/Formality-JavaScript/issues). If you see our command-line instructions, Formality-Core has been successfully installed in your system. If you have any problem during this process, please [open an issue](https://github.com/moonad/Formality/issues).
[< Why Formality](https://github.com/moonad/Formality-JavaScript/wiki) | [Hello World >](https://github.com/moonad/Formality-JavaScript/wiki/Hello,-world!) [< Why Formality](https://github.com/moonad/Formality/wiki) | [Hello World >](https://github.com/moonad/Formality/wiki/Hello,-world!)

2
Lambdas-and-Affinity.md

@ -67,4 +67,4 @@ The first two are preferable because they avoid using boxes. A general rule is:
Despite affine lambdas being somewhat hard to work with, they're part of the reason Formality has so great computational characteristics. Moreover, they're not as restrictive as they seem. In fact, almost any non-terminating program that you'd use in practice can be written in Formality-Core with clever use of boxes (technically, any one that terminates in `2^(2^(2^...n))` steps, where `n` is the program size and the number of `2`s is equal to its depth). Despite affine lambdas being somewhat hard to work with, they're part of the reason Formality has so great computational characteristics. Moreover, they're not as restrictive as they seem. In fact, almost any non-terminating program that you'd use in practice can be written in Formality-Core with clever use of boxes (technically, any one that terminates in `2^(2^(2^...n))` steps, where `n` is the program size and the number of `2`s is equal to its depth).
[< Dups and Boxes](https://github.com/moonad/Formality-JavaScript/wiki/Dups-and-Boxes) | [Data types >](https://github.com/moonad/Formality-JavaScript/wiki/Datatypes) [< Dups and Boxes](https://github.com/moonad/Formality/wiki/Dups-and-Boxes) | [Data types >](https://github.com/moonad/Formality/wiki/Datatypes)

2
Lets-and-Defs.md

@ -32,4 +32,4 @@ def main:
|year - age|] |year - age|]
``` ```
[< Pairs](https://github.com/moonad/Formality-JavaScript/wiki/Pairs) | [If and Cpy >](https://github.com/moonad/Formality-JavaScript/wiki/If-and-Cpy) [< Pairs](https://github.com/moonad/Formality/wiki/Pairs) | [If and Cpy >](https://github.com/moonad/Formality/wiki/If-and-Cpy)

2
Numbers-and-Operators.md

@ -41,4 +41,4 @@ greater-than | `\|x > y\|` | `x > y ? 1 : 0`
less-than | `\|x < y\|` | `x < y ? 1 : 0` less-than | `\|x < y\|` | `x < y ? 1 : 0`
equals | `\|x == y\|` | `x === y ? 1 : 0` equals | `\|x == y\|` | `x === y ? 1 : 0`
[< Hello World](https://github.com/moonad/Formality-JavaScript/wiki/Hello,-world!) | [Pair >](https://github.com/moonad/Formality-JavaScript/wiki/Pairs) [< Hello World](https://github.com/moonad/Formality/wiki/Hello,-world!) | [Pair >](https://github.com/moonad/Formality/wiki/Pairs)

2
Pairs.md

@ -81,4 +81,4 @@ def main:
The program above outputs `1`. The program above outputs `1`.
[< Numbers and Operators](https://github.com/moonad/Formality-JavaScript/wiki/Numbers-and-Operators) | [Lets and Defs >](https://github.com/moonad/Formality-JavaScript/wiki/Lets-and-Defs) [< Numbers and Operators](https://github.com/moonad/Formality/wiki/Numbers-and-Operators) | [Lets and Defs >](https://github.com/moonad/Formality/wiki/Lets-and-Defs)

2
Undefined-Behavior.md

@ -24,4 +24,4 @@ If you try to evaluate it with interaction nets, it will output `[6,6]`, which i
Similar situations can happen when trying to duplicate a term that isn't inside a box. Boxes are fully erased after compilation, so, interaction nets won't display a nice error message in those cases. Instead, they will go ahead copying the unboxed lambda, and anything can happen afterwards. Be very cautious with copies and always use the interpreter to make sure you're not trying to copy an unboxed value! Similar situations can happen when trying to duplicate a term that isn't inside a box. Boxes are fully erased after compilation, so, interaction nets won't display a nice error message in those cases. Instead, they will go ahead copying the unboxed lambda, and anything can happen afterwards. Be very cautious with copies and always use the interpreter to make sure you're not trying to copy an unboxed value!
[< Bounded Loops and Recursion](https://github.com/moonad/Formality-JavaScript/wiki/Bounded-Loops-and-Recursion) | [Formality Interaction Nets >](https://github.com/moonad/Formality-JavaScript/wiki/Formality-Interaction-Net-System-(FINS)) [< Bounded Loops and Recursion](https://github.com/moonad/Formality/wiki/Bounded-Loops-and-Recursion) | [Formality Interaction Nets >](https://github.com/moonad/Formality/wiki/Formality-Interaction-Net-System-(FINS))

2
[pt-br]-0.-Instalação.md

@ -9,4 +9,4 @@ fmc
Se aparecer nossas instruções no Terminal, o Formality-Core foi instalado com sucesso em seu sistema. Se você tiver algum problema durante este processo, por favor [abrir uma issue] (https://github.com/moonad/formality-core/issues). Se aparecer nossas instruções no Terminal, o Formality-Core foi instalado com sucesso em seu sistema. Se você tiver algum problema durante este processo, por favor [abrir uma issue] (https://github.com/moonad/formality-core/issues).
[< Por que Formality Core?](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-Por-que-Formality-Core%3F) | [Hello, World! >](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-1.-Hello,-World!) [< Por que Formality Core?](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-Por-que-Formality-Core%3F) | [Hello, World! >](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-1.-Hello,-World!)

2
[pt-br]-1.-Hello,-World!.md

@ -7,4 +7,4 @@ def main:
Salve como `main.fmc` e usando o terminal, vá para o diretório onde você salvou o arquivo, então execute-o com o `fmc main`. Se você ver "Hello, world!" no seu terminal, então funcionou. Você também pode inserir apenas `fmc` para ver a lista de opções. Oferecemos suporte a vários evaluators, incluindo um interpretador, lazy/strict interaction net e até closures nativas de JS, todos com características diferentes. Salve como `main.fmc` e usando o terminal, vá para o diretório onde você salvou o arquivo, então execute-o com o `fmc main`. Se você ver "Hello, world!" no seu terminal, então funcionou. Você também pode inserir apenas `fmc` para ver a lista de opções. Oferecemos suporte a vários evaluators, incluindo um interpretador, lazy/strict interaction net e até closures nativas de JS, todos com características diferentes.
[< Instalação](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-0.-Instalação) | [Números e Operadores >](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-2.-Números-e-operadores) [< Instalação](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-0.-Instalação) | [Números e Operadores >](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-2.-Números-e-operadores)

2
[pt-br]-2.-Números-e-operadores.md

@ -39,4 +39,4 @@ maior-que | `\|x > y\|` | `x > y ? 1 : 0`
menor-que | `\|x < y\|` | `x < y ? 1 : 0` menor-que | `\|x < y\|` | `x < y ? 1 : 0`
igual | `\|x == y\|` | `x === y ? 1 : 0` igual | `\|x == y\|` | `x === y ? 1 : 0`
[< Hello, World](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-1.-Hello,-World!) | [Pares >](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-3.-Pares) [< Hello, World](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-1.-Hello,-World!) | [Pares >](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-3.-Pares)

2
[pt-br]-4.-Lets-e-Defs.md

@ -28,4 +28,4 @@ def main:
|year - age|] |year - age|]
``` ```
[< Pares](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-3.-Pares) | [If e Cpy >](https://github.com/moonad/formality-core/wiki/If-and-Cpy) [< Pares](https://github.com/moonad/Formality-Core/wiki/%5Bpt-br%5D-3.-Pares) | [If e Cpy >](https://github.com/moonad/formality-core/wiki/If-and-Cpy)

2
_Footer.md

@ -1 +1 @@
[Português-br](https://github.com/moonad/Formality-Core/wiki/%5Bpt%5D-Por-que-Formality-Core%3F) | [Português-br](https://github.com/moonad/Formality-Core/wiki/%5Bpt%5D-Por-que-Formality-Core%3F) |